import com.microsoft.z3.Context; //导入依赖的package包/类
private Model check(Context ctx, BoolExpr f, Status sat, Solver s){
	try{
		s.push();
		s.add(f);

		if (s.check() != sat){
			s.pop();

			return null;
		}else if (sat == Status.SATISFIABLE){
			Model ret = s.getModel();
			s.pop();

			return ret;
		}else{
			new java.lang.Exception().printStackTrace();
			System.exit(1);
			return null;
		}
	}catch(Exception e){
		e.printStackTrace();
		System.out.println("Hey dummy");
		System.exit(1);
		return null;
	}
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
@Test
public void test() {
	final Context context = new Context();
	final Solver solver = context.mkSimpleSolver();

	final BoolExpr a = context.mkBoolConst("a");
	final BoolExpr b = context.mkBoolConst("b");
	final BoolExpr expr = context.mkOr(a, b);

	solver.add(expr);
	solver.check();
	final Model model = solver.getModel();

	System.out.println(model.getConstInterp(a));
	System.out.println(model.getConstInterp(b));

	context.close();
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
public NativeZ3Solver(int to, Map<String, String> properties) {
  this.timeout = to;
  this.options = properties;

  Map<String, String> cfg = Collections.singletonMap("model", "true");
  for (Entry<String, String> o : options.entrySet()) {
    Global.setParameter(o.getKey(), o.getValue());
  }

  try {
    this.ctx = new Context(cfg);
    defaultContext = createContext();
  } catch (Z3Exception ex) {
    if (ctx != null) {
      try {
        ctx.dispose();
      } catch (Throwable t) {
      }
    }
    throw new RuntimeException(ex);
  }
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
public @NonNull Z3Model firstCheckSatAndGetModel(@NonNull String smtEncoding) {

		Map<String, String> config = new HashMap<>();
		config.put("model", "true");
		try {
			context = new Context(config);
			solver = context.mkSolver();
			sorts = new ArrayDeque<>();
			decls = new ArrayDeque<>();

			return runCheckSatAndGetModel(smtEncoding);
		}
		catch (Z3Exception e) {
			MMINTException.print(IStatus.WARNING, "Z3 problem, returning unknown result and resetting the solver", e);
			reset();
			return new Z3Model(Status.UNKNOWN, null);
		}
	}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
public ModelZ3JavaService(Green solver, Properties properties) {
	super(solver);
	HashMap<String, String> cfg = new HashMap<String, String>();
       cfg.put("model", "true");
	try{
		ctx = new Context(cfg);		 
	} catch (Exception e) {
		e.printStackTrace();
		throw new RuntimeException("## Error Z3: Exception caught in Z3 JNI: \n" + e);
    }
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
public SATZ3JavaService(Green solver, Properties properties) {
	super(solver);
	HashMap<String, String> cfg = new HashMap<String, String>();
       cfg.put("model", "true");
	try{
		ctx = new Context(cfg);		 
	} catch (Exception e) {
		e.printStackTrace();
		throw new RuntimeException("## Error Z3: Exception caught in Z3 JNI: \n" + e);
    }
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
public SubsumptionHelper(){
	cfgModel = new HashMap<String, String>();
	cfgModel.put("model", "true");

	try{
		mainCtx = new Context(cfgModel);
		mainSolver = mainCtx.mkSolver();
	}catch(Z3Exception e){
		e.printStackTrace();
		System.exit(1);
	}
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
Z3DeclTransformer(final Z3TransformationManager transformer, final Z3SymbolTable symbolTable,
		final Context context) {
	this.transformer = transformer;
	this.symbolTable = symbolTable;
	this.context = context;
	this.symbolCount = 0;
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
Z3TypeTransformer(final Z3TransformationManager transformer, final Context context) {
	this.context = context;
	this.transformer = transformer;

	boolSort = context.mkBoolSort();
	intSort = context.mkIntSort();
	realSort = context.mkRealSort();
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
public NativeZ3ExpressionGenerator(Context ctx, Solver solver)
		throws Z3Exception {
	this.ctx = ctx;
	this.solver = solver;
	this.protect = new HashSet<IDisposable>();
	this.tainted = (BoolExpr)ctx.mkFreshConst("__tainted", ctx.getBoolSort());
	this.protect.add(tainted);
	this.own.add(tainted);
	this.variables = new HashMap<Variable<?>, Expr>();
	
	this.count = 0;
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
private Solver loadSMTLIBEncoding(Map<String, String> config, String smtEncoding) throws Z3Exception {

		Context context = new Context(config);
		Solver solver = context.mkSolver();
		BoolExpr expr = context.parseSMTLIB2String(smtEncoding, null, null, null, null);
		solver.add(expr);

		return solver;
	}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
@Before
public void setUp() {
  ctx = new Context();
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
public Z3JavaTranslator(Context c) {
	this.context = c;
	stack = new Stack<Expr>();
	v2e = new HashMap<Variable, Expr>();
	domains = new LinkedList<BoolExpr>();
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
private BoolExpr exploreExpression(Expression e, Context ctx) throws Z3Exception{
	Explorer ex = new Explorer(ctx);
	return ex.explore(e);
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
public Explorer(Context ctx){
	this.ctx = ctx; 
	this.stack = new Stack<Expr>();
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
public Z3TransformationManager(final Z3SymbolTable symbolTable, final Context context) {
	this.typeTransformer = new Z3TypeTransformer(this, context);
	this.declTransformer = new Z3DeclTransformer(this, symbolTable, context);
	this.exprTransformer = new Z3ExprTransformer(this, context);
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
Context getContext() {
  return ctx;
}
 

import com.microsoft.z3.Context; //导入依赖的package包/类
public SolverWrapperZ3() throws Z3Exception{
	Map<String, String> cfg = new HashMap<String, String>();
	ctx = new Context(cfg);
	sootVarToZ3Var = new HashMap<Value,IntExpr>();
}