@Test public void testEquality() { ArrayList<Node> clauses = new ArrayList<>(); ProgramVariable x = ProgramVariable.mkInt("x"); ProgramVariable y = ProgramVariable.mkInt("y"); clauses.add(new Equal(x, y)); clauses.add(new Equal(x, IntConst.of(5))); Optional<Map<Variable, Constant>> result = solver.sat(clauses); assertTrue(result.isPresent()); assertEquals(result.get().get(y), IntConst.of(5)); }
@Override public Optional<Map<Variable, Constant>> sat(List<Node> clauses) { com.microsoft.z3.Solver solver = ctx.mkSolver(); VariableMarshaller marshaller = new VariableMarshaller(); for (Node clause : clauses) { solver.add(toZ3(marshaller, clause)); } Status status = solver.check(); if (status.equals(Status.SATISFIABLE)) { Model model = solver.getModel(); return Optional.of(getAssignment(model, marshaller)); } else if (status.equals(Status.UNSATISFIABLE)) { return Optional.empty(); } else { throw new UnsupportedOperationException(); } }
Z3 implements Solver { @Override public Optional<Map<Variable, Constant>> sat(List<Node> clauses) { com.microsoft.z3.Solver solver = ctx.mkSolver(); VariableMarshaller marshaller = new VariableMarshaller(); for (Node clause : clauses) { solver.add(toZ3(marshaller, clause)); } Status status = solver.check(); if (status.equals(Status.SATISFIABLE)) { Model model = solver.getModel(); return Optional.of(getAssignment(model, marshaller)); } else if (status.equals(Status.UNSATISFIABLE)) { return Optional.empty(); } else { throw new UnsupportedOperationException(); } } }
Z3 implements Solver { @Override public Optional<Map<Variable, Constant>> sat(List<Node> clauses) { com.microsoft.z3.Solver solver = ctx.mkSolver(); VariableMarshaller marshaller = new VariableMarshaller(); for (Node clause : clauses) { solver.add(toZ3(marshaller, clause)); } Status status = solver.check(); if (status.equals(Status.SATISFIABLE)) { Model model = solver.getModel(); return Optional.of(getAssignment(model, marshaller)); } else if (status.equals(Status.UNSATISFIABLE)) { return Optional.empty(); } else { throw new UnsupportedOperationException(); } } Z3(); }
Z3 implements Solver { @Override public Optional<Map<Variable, Constant>> sat(List<Node> clauses) { com.microsoft.z3.Solver solver = ctx.mkSolver(); VariableMarshaller marshaller = new VariableMarshaller(); for (Node clause : clauses) { solver.add(toZ3(marshaller, clause)); } Status status = solver.check(); if (status.equals(Status.SATISFIABLE)) { Model model = solver.getModel(); return Optional.of(getAssignment(model, marshaller)); } else if (status.equals(Status.UNSATISFIABLE)) { return Optional.empty(); } else { throw new UnsupportedOperationException(); } } Z3(); void enableCustomMaxsatWithBound(int i); void disableCustomMaxsat(); @Override Optional<Map<Variable, Constant>> maxsat(List<Node> hard, List<Node> soft); @Override Optional<Map<Variable, Constant>> sat(List<Node> clauses); }
Z3 implements Solver { @Override public Optional<Map<Variable, Constant>> sat(List<Node> clauses) { com.microsoft.z3.Solver solver = ctx.mkSolver(); VariableMarshaller marshaller = new VariableMarshaller(); for (Node clause : clauses) { solver.add(toZ3(marshaller, clause)); } Status status = solver.check(); if (status.equals(Status.SATISFIABLE)) { Model model = solver.getModel(); return Optional.of(getAssignment(model, marshaller)); } else if (status.equals(Status.UNSATISFIABLE)) { return Optional.empty(); } else { throw new UnsupportedOperationException(); } } Z3(); void enableCustomMaxsatWithBound(int i); void disableCustomMaxsat(); @Override Optional<Map<Variable, Constant>> maxsat(List<Node> hard, List<Node> soft); @Override Optional<Map<Variable, Constant>> sat(List<Node> clauses);  }