@Test public void testTrack() { final Solver solver = Z3SolverFactory.getInstance().createSolver(); final ConstDecl<BoolType> ca = Const("a", BoolExprs.Bool()); final Expr<BoolType> expr = BoolExprs.And(ca.getRef(), True()); solver.push(); solver.track(expr); final SolverStatus status = solver.check(); assertTrue(status.isSat()); final Valuation model = solver.getModel(); assertNotNull(model); solver.pop(); }
@Override public void track(final Expr<BoolType> assertion) { checkNotNull(assertion); assertions.add(assertion); final com.microsoft.z3.BoolExpr term = (com.microsoft.z3.BoolExpr) transformationManager.toTerm(assertion); final String label = String.format(ASSUMPTION_LABEL, labelNum++); final com.microsoft.z3.BoolExpr labelTerm = z3Context.mkBoolConst(label); assumptions.put(label, assertion); z3Solver.assertAndTrack(term, labelTerm); clearState(); }
Z3Solver implements Solver { @Override public void track(final Expr<BoolType> assertion) { checkNotNull(assertion); assertions.add(assertion); final com.microsoft.z3.BoolExpr term = (com.microsoft.z3.BoolExpr) transformationManager.toTerm(assertion); final String label = String.format(ASSUMPTION_LABEL, labelNum++); final com.microsoft.z3.BoolExpr labelTerm = z3Context.mkBoolConst(label); assumptions.put(label, assertion); z3Solver.assertAndTrack(term, labelTerm); clearState(); } }
Z3Solver implements Solver { @Override public void track(final Expr<BoolType> assertion) { checkNotNull(assertion); assertions.add(assertion); final com.microsoft.z3.BoolExpr term = (com.microsoft.z3.BoolExpr) transformationManager.toTerm(assertion); final String label = String.format(ASSUMPTION_LABEL, labelNum++); final com.microsoft.z3.BoolExpr labelTerm = z3Context.mkBoolConst(label); assumptions.put(label, assertion); z3Solver.assertAndTrack(term, labelTerm); clearState(); } Z3Solver(final Z3SymbolTable symbolTable, final Z3TransformationManager transformationManager,
					final Z3TermTransformer termTransformer, final com.microsoft.z3.Context z3Context,
					final com.microsoft.z3.Solver z3Solver); }
Z3Solver implements Solver { @Override public void track(final Expr<BoolType> assertion) { checkNotNull(assertion); assertions.add(assertion); final com.microsoft.z3.BoolExpr term = (com.microsoft.z3.BoolExpr) transformationManager.toTerm(assertion); final String label = String.format(ASSUMPTION_LABEL, labelNum++); final com.microsoft.z3.BoolExpr labelTerm = z3Context.mkBoolConst(label); assumptions.put(label, assertion); z3Solver.assertAndTrack(term, labelTerm); clearState(); } Z3Solver(final Z3SymbolTable symbolTable, final Z3TransformationManager transformationManager,
					final Z3TermTransformer termTransformer, final com.microsoft.z3.Context z3Context,
					final com.microsoft.z3.Solver z3Solver); @Override void add(final Expr<BoolType> assertion); @Override void track(final Expr<BoolType> assertion); @Override SolverStatus check(); @Override void push(); @Override void pop(final int n); @Override void reset(); @Override SolverStatus getStatus(); @Override Valuation getModel(); @Override Collection<Expr<BoolType>> getUnsatCore(); @Override Collection<Expr<BoolType>> getAssertions(); }
Z3Solver implements Solver { @Override public void track(final Expr<BoolType> assertion) { checkNotNull(assertion); assertions.add(assertion); final com.microsoft.z3.BoolExpr term = (com.microsoft.z3.BoolExpr) transformationManager.toTerm(assertion); final String label = String.format(ASSUMPTION_LABEL, labelNum++); final com.microsoft.z3.BoolExpr labelTerm = z3Context.mkBoolConst(label); assumptions.put(label, assertion); z3Solver.assertAndTrack(term, labelTerm); clearState(); } Z3Solver(final Z3SymbolTable symbolTable, final Z3TransformationManager transformationManager,
					final Z3TermTransformer termTransformer, final com.microsoft.z3.Context z3Context,
					final com.microsoft.z3.Solver z3Solver); @Override void add(final Expr<BoolType> assertion); @Override void track(final Expr<BoolType> assertion); @Override SolverStatus check(); @Override void push(); @Override void pop(final int n); @Override void reset(); @Override SolverStatus getStatus(); @Override Valuation getModel(); @Override Collection<Expr<BoolType>> getUnsatCore(); @Override Collection<Expr<BoolType>> getAssertions();  }