diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 0847bc868..e1b5fb6d8 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -2010,6 +2010,47 @@ namespace test_mapi } } + /// + /// Extract unsatisfiable core example with AssertAndTrack + /// + public static void UnsatCoreAndProofExample2(Context ctx) + { + Console.WriteLine("UnsatCoreAndProofExample2"); + + Solver solver = ctx.MkSolver(); + + BoolExpr pa = ctx.MkBoolConst("PredA"); + BoolExpr pb = ctx.MkBoolConst("PredB"); + BoolExpr pc = ctx.MkBoolConst("PredC"); + BoolExpr pd = ctx.MkBoolConst("PredD"); + + BoolExpr f1 = ctx.MkAnd(new BoolExpr[] { pa, pb, pc }); + BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc }); + BoolExpr f3 = ctx.MkOr(ctx.MkNot(pa), ctx.MkNot(pc)); + BoolExpr f4 = pd; + + BoolExpr p1 = ctx.MkBoolConst("P1"); + BoolExpr p2 = ctx.MkBoolConst("P2"); + BoolExpr p3 = ctx.MkBoolConst("P3"); + BoolExpr p4 = ctx.MkBoolConst("P4"); + + solver.AssertAndTrack(f1, p1); + solver.AssertAndTrack(f2, p2); + solver.AssertAndTrack(f3, p3); + solver.AssertAndTrack(f4, p4); + Status result = solver.Check(); + + if (result == Status.UNSATISFIABLE) + { + Console.WriteLine("unsat"); + Console.WriteLine("core: "); + foreach (Expr c in solver.UnsatCore) + { + Console.WriteLine("{0}", c); + } + } + } + public static void FiniteDomainExample(Context ctx) { Console.WriteLine("FiniteDomainExample"); @@ -2164,6 +2205,7 @@ namespace test_mapi TreeExample(ctx); ForestExample(ctx); UnsatCoreAndProofExample(ctx); + UnsatCoreAndProofExample2(ctx); } // These examples need proof generation turned on and auto-config set to false. diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index d23f249de..5c49b56ae 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -2137,6 +2137,47 @@ class JavaExample } } } + + /// Extract unsatisfiable core example with AssertAndTrack + + public void unsatCoreAndProofExample2(Context ctx) throws Z3Exception + { + System.out.println("UnsatCoreAndProofExample2"); + Log.append("UnsatCoreAndProofExample2"); + + Solver solver = ctx.mkSolver(); + + BoolExpr pa = ctx.mkBoolConst("PredA"); + BoolExpr pb = ctx.mkBoolConst("PredB"); + BoolExpr pc = ctx.mkBoolConst("PredC"); + BoolExpr pd = ctx.mkBoolConst("PredD"); + + BoolExpr f1 = ctx.mkAnd(new BoolExpr[] { pa, pb, pc }); + BoolExpr f2 = ctx.mkAnd(new BoolExpr[] { pa, ctx.mkNot(pb), pc }); + BoolExpr f3 = ctx.mkOr(ctx.mkNot(pa), ctx.mkNot(pc)); + BoolExpr f4 = pd; + + BoolExpr p1 = ctx.mkBoolConst("P1"); + BoolExpr p2 = ctx.mkBoolConst("P2"); + BoolExpr p3 = ctx.mkBoolConst("P3"); + BoolExpr p4 = ctx.mkBoolConst("P4"); + + solver.assertAndTrack(f1, p1); + solver.assertAndTrack(f2, p2); + solver.assertAndTrack(f3, p3); + solver.assertAndTrack(f4, p4); + Status result = solver.check(); + + if (result == Status.UNSATISFIABLE) + { + System.out.println("unsat"); + System.out.println("core: "); + for (Expr c : solver.getUnsatCore()) + { + System.out.println(c); + } + } + } public void finiteDomainExample(Context ctx) throws Z3Exception { @@ -2298,6 +2339,7 @@ class JavaExample p.treeExample(ctx); p.forestExample(ctx); p.unsatCoreAndProofExample(ctx); + p.unsatCoreAndProofExample2(ctx); } { // These examples need proof generation turned on and auto-config diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index dfbb62f65..649a79be2 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -178,8 +178,9 @@ public: virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { m_check_sat_executed = true; - - if (num_assumptions > 0 || // assumptions were provided + + if (get_num_assumptions() != 0 || + num_assumptions > 0 || // assumptions were provided m_ignore_solver1) { // must use incremental solver switch_inc_mode(); @@ -241,6 +242,16 @@ public: return m_solver1->get_assertion(idx); } + virtual unsigned get_num_assumptions() const { + return m_solver1->get_num_assumptions() + m_solver2->get_num_assumptions(); + } + + virtual expr * get_assumption(unsigned idx) const { + unsigned c1 = m_solver1->get_num_assumptions(); + if (idx < c1) return m_solver1->get_assumption(idx); + return m_solver2->get_assumption(idx - c1); + } + virtual void display(std::ostream & out) const { m_solver1->display(out); } diff --git a/src/solver/solver.h b/src/solver/solver.h index a95c649c0..b5a407e2a 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -72,7 +72,7 @@ public: /** \brief Add a new formula \c t to the assertion stack, and "tag" it with \c a. - The propositional varialbe \c a is used to track the use of \c t in a proof + The propositional variable \c a is used to track the use of \c t in a proof of unsatisfiability. */ virtual void assert_expr(expr * t, expr * a) = 0; @@ -125,6 +125,16 @@ public: */ virtual expr * get_assertion(unsigned idx) const; + /** + \brief The number of tracked assumptions (see assert_expr(t, a)). + */ + virtual unsigned get_num_assumptions() const = 0; + + /** + \brief Retrieves the idx'th tracked assumption (see assert_expr(t, a)). + */ + virtual expr * get_assumption(unsigned idx) const = 0; + /** \brief Display the content of this solver. */ diff --git a/src/solver/solver_na2as.h b/src/solver/solver_na2as.h index 15750344a..4c6af0dca 100644 --- a/src/solver/solver_na2as.h +++ b/src/solver/solver_na2as.h @@ -41,6 +41,9 @@ public: virtual void push(); virtual void pop(unsigned n); virtual unsigned get_scope_level() const; + + virtual unsigned get_num_assumptions() const { return m_assumptions.size(); } + virtual expr * get_assumption(unsigned idx) const { return m_assumptions[idx]; } protected: virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0; virtual void push_core() = 0;