import ap.parser.IExpression; //导入依赖的package包/类
@Override
public IFormula and(IExpression t1, IExpression t2) {
  if (t1 == t2) {
    return (IFormula) t1;
  }
  if (isTrue(t1)) {
    return (IFormula) t2;
  }
  if (isTrue(t2)) {
    return (IFormula) t1;
  }
  if (isFalse(t1)) {
    return pFalse;
  }
  if (isFalse(t2)) {
    return pFalse;
  }
  return simplify(new IBinFormula(IBinJunctor.And(), (IFormula) t1, (IFormula) t2));
}
 

import ap.parser.IExpression; //导入依赖的package包/类
@Override
public IFormula or(IExpression t1, IExpression t2) {
  if (t1 == t2) {
    return (IFormula) t1;
  }
  if (isTrue(t1)) {
    return pTrue;
  }
  if (isTrue(t2)) {
    return pTrue;
  }
  if (isFalse(t1)) {
    return (IFormula) t2;
  }
  if (isFalse(t2)) {
    return (IFormula) t1;
  }
  return simplify(new IBinFormula(IBinJunctor.Or(), (IFormula) t1, (IFormula) t2));
}
 

import ap.parser.IExpression; //导入依赖的package包/类
/**
 * Collect array-models, we need them to replace identifiers later. Princess models arrays as
 * plain numeric "memory-addresses", and the model for an array-access at one of the addresses is
 * the array-content. Example: "arr[5]=123" is modeled as "{arr=0, select(0,5)=123}" or "{arr=0,
 * store(0,5,123)=0}", where "0" is the memory-address. The returned mapping contains the mapping
 * of "0" (=address) to "arr" (=identifier).
 */
private Map<IdealInt, ITerm> getArrayAddresses(
    scala.collection.Map<ModelLocation, ModelValue> interpretation) {
  Map<IdealInt, ITerm> arrays = new HashMap<>();
  Iterator<Tuple2<ModelLocation, ModelValue>> it1 = interpretation.iterator();
  while (it1.hasNext()) {
    Tuple2<ModelLocation, ModelValue> entry = it1.next();
    if (entry._1 instanceof ConstantLoc) {
      ITerm maybeArray = IExpression.i(((ConstantLoc) entry._1).c());
      if (creator.getEnv().hasArrayType(maybeArray) && entry._2 instanceof IntValue) {
        arrays.put(((IntValue) entry._2).v(), maybeArray);
      }
    }
  }
  return arrays;
}
 

import ap.parser.IExpression; //导入依赖的package包/类
public ProverExpr mkTrigger(ProverExpr body, ProverExpr[] triggers) {
  final ArrayBuffer<IExpression> triggerExprs = new ArrayBuffer<IExpression> ();
  
  for (int i = 0; i < triggers.length; ++i) {
    if (triggers[i] instanceof TermExpr)
      triggerExprs.$plus$eq(((TermExpr)triggers[i]).term);
    else
         triggerExprs.$plus$eq(((FormulaExpr)triggers[i]).formula);
  }
  
  return new FormulaExpr(IExpression.trig(((FormulaExpr)body).formula,
                                          triggerExprs));
}
 

import ap.parser.IExpression; //导入依赖的package包/类
@Override
protected IExpression simplify(IExpression f) {
  // TODO this method is not tested, check it!
  if (f instanceof IFormula) {
    f = BooleanCompactifier.apply((IFormula) f);
  }
  return PartialEvaluator.apply(f);
}
 

import ap.parser.IExpression; //导入依赖的package包/类
PrincessArrayFormulaManager(
    FormulaCreator<
            IExpression, PrincessTermType, PrincessEnvironment, PrincessFunctionDeclaration>
        pFormulaCreator) {
  super(pFormulaCreator);
  env = pFormulaCreator.getEnv();
}
 

import ap.parser.IExpression; //导入依赖的package包/类
@Override
protected <TI extends Formula, TE extends Formula> IExpression internalMakeArray(
    String pName, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {

  // other types in arrays are not supported in princess
  assert pIndexType.isIntegerType() && pElementType.isIntegerType();

  final ArrayFormulaType<TI, TE> arrayFormulaType =
      FormulaType.getArrayType(pIndexType, pElementType);
  final PrincessTermType arrayType = toSolverType(arrayFormulaType);

  return getFormulaCreator().makeVariable(arrayType, pName);
}
 

import ap.parser.IExpression; //导入依赖的package包/类
@Override
public IExpression makeApp(PrincessEnvironment env, List<IExpression> args) {
  Preconditions.checkArgument(args.size() == 2);
  if (args.get(0) instanceof IIntLit) {
    return new ITimes(((IIntLit) args.get(0)).value(), (ITerm) args.get(1));
  } else if (args.get(1) instanceof IIntLit) {
    return new ITimes(((IIntLit) args.get(1)).value(), (ITerm) args.get(0));
  } else {
    throw new AssertionError("unexpected args for multiplication");
  }
}
 

import ap.parser.IExpression; //导入依赖的package包/类
@Override
public IExpression ifThenElse(IExpression condition, IExpression t1, IExpression t2) {
  if (t1 instanceof IFormula) {
    return new IFormulaITE((IFormula) condition, (IFormula) t1, (IFormula) t2);
  } else {
    return new ITermITE((IFormula) condition, (ITerm) t1, (ITerm) t2);
  }
}
 

import ap.parser.IExpression; //导入依赖的package包/类
@Override
public IFormula not(IExpression pBits) {
  if (pBits instanceof INot) {
    return ((INot) pBits).subformula(); // "not not a" == "a"
  } else {
    return new INot((IFormula) pBits);
  }
}
 

import ap.parser.IExpression; //导入依赖的package包/类
@Nullable
@Override
public Object evaluateImpl(IExpression f) {
  Option<ModelValue> out = model.evalExpression(f);
  if (out.isEmpty()) {
    return null;
  }
  ModelValue value = out.get();
  return getValue(value);
}
 

import ap.parser.IExpression; //导入依赖的package包/类
@Override
public IExpression multiply(IExpression pNumber1, IExpression pNumber2) {
  IExpression result;
  try {
    result = ((ITerm) pNumber1).$times((ITerm) pNumber2);
  } catch (IllegalArgumentException e) {
    result = BitShiftMultiplication.mult((ITerm) pNumber1, (ITerm) pNumber2);
  }
  return result;
}
 

import ap.parser.IExpression; //导入依赖的package包/类
@Override
public List<BooleanFormula> getUnsatCore() {
  Preconditions.checkState(!closed && computeUnsatCores);
  final List<BooleanFormula> result = new ArrayList<>();
  final scala.collection.immutable.Set<Object> core = api.getUnsatCore();

  int cnt = 0;
  for (IExpression formula : getAssertedFormulas()) {
    if (core.contains(cnt)) {
      result.add(mgr.encapsulateBooleanFormula(formula));
    }
    ++cnt;
  }
  return result;
}
 

import ap.parser.IExpression; //导入依赖的package包/类
public List<? extends IExpression> parseStringToTerms(String s, PrincessFormulaCreator creator) {

    Tuple3<
            Seq<IFormula>, scala.collection.immutable.Map<IFunction, SMTFunctionType>,
            scala.collection.immutable.Map<ConstantTerm, SMTType>>
        triple = api.extractSMTLIBAssertionsSymbols(new StringReader(s));

    List<? extends IExpression> formula = seqAsJavaList(triple._1());
    Map<IFunction, SMTFunctionType> functionTypes = mapAsJavaMap(triple._2());
    Map<ConstantTerm, SMTType> constantTypes = mapAsJavaMap(triple._3());

    ImmutableSet.Builder<IExpression> declaredFunctions = ImmutableSet.builder();
    for (IExpression f : formula) {
      declaredFunctions.addAll(creator.extractVariablesAndUFs(f, true).values());
    }
    for (IExpression var : declaredFunctions.build()) {
      if (var instanceof IConstant) {
        SMTType type = constantTypes.get(((IConstant) var).c());
        if (type instanceof SMTParser2InputAbsy.SMTArray) {
          arrayVariablesCache.put(var.toString(), (ITerm) var);
        } else {
          intVariablesCache.put(var.toString(), (ITerm) var);
        }
        addSymbol((IConstant) var);
      } else if (var instanceof IAtom) {
        boolVariablesCache.put(((IAtom) var).pred().name(), (IFormula) var);
        addSymbol((IAtom) var);
      } else if (var instanceof IFunApp) {
        IFunction fun = ((IFunApp) var).fun();
        functionsCache.put(fun.name(), fun);
        functionsReturnTypes.put(fun, convertToTermType(functionTypes.get(fun)));
        addFunction(fun);
      }
    }
    return formula;
  }
 

import ap.parser.IExpression; //导入依赖的package包/类
private static String getName(IExpression var) {
  if (var instanceof IAtom) {
    return ((IAtom) var).pred().name();
  } else if (var instanceof IConstant) {
    return var.toString();
  } else if (var instanceof IFunApp) {
    String fullStr = ((IFunApp) var).fun().toString();
    return fullStr.substring(0, fullStr.indexOf('/'));
  }

  throw new IllegalArgumentException("The given parameter is no variable or function");
}
 

import ap.parser.IExpression; //导入依赖的package包/类
private static String getType(IExpression var) {
  if (var instanceof IFormula) {
    return "Bool";

    // functions are included here, they cannot be handled separate for princess
  } else if (var instanceof ITerm) {
    return "Int";
  }

  throw new IllegalArgumentException("The given parameter is no variable or function");
}
 

import ap.parser.IExpression; //导入依赖的package包/类
PrincessQuantifiedFormulaManager(
    FormulaCreator<
            IExpression, PrincessTermType, PrincessEnvironment, PrincessFunctionDeclaration>
        pCreator) {
  super(pCreator);
  env = getFormulaCreator().getEnv();
}
 

import ap.parser.IExpression; //导入依赖的package包/类
@Override
public IExpression mkQuantifier(Quantifier q, List<IExpression> vars, IExpression body) {
  checkArgument(body instanceof IFormula);
  ap.terfor.conjunctions.Quantifier pq = (q == Quantifier.FORALL) ? ALL$.MODULE$ : EX$.MODULE$;
  if (vars.size() == 0) {

    // Body already contains bound variables.
    return new IQuantified(pq, (IFormula) body);
  } else {
    return IExpression.quanConsts(
        pq, iterableAsScalaIterable(toConstantTerm(vars)), (IFormula) body);
  }
}
 

import ap.parser.IExpression; //导入依赖的package包/类
private List<ConstantTerm> toConstantTerm(List<IExpression> lst) {
  List<ConstantTerm> retVal = new ArrayList<>(lst.size());
  for (IExpression f : lst) {
    retVal.add(((IConstant) f).c());
  }
  return retVal;
}
 

import ap.parser.IExpression; //导入依赖的package包/类
@Override
public FormulaType<?> getFormulaType(IExpression pFormula) {
  if (getEnv().hasArrayType(pFormula)) {
    return new ArrayFormulaType<>(FormulaType.IntegerType, FormulaType.IntegerType);
  } else if (pFormula instanceof IFormula) {
    return FormulaType.BooleanType;
  } else if (pFormula instanceof ITerm) {
    return FormulaType.IntegerType;
  }
  throw new IllegalArgumentException("Unknown formula type");
}