Bugfix and new examples for implicit assumptions in Z3_solver_assert_and_track. Thanks to Amir Ebrahimi for reporting this issue!

(See http://stackoverflow.com/questions/28558683/modeling-constraints-in-z3-and-unsat-core-cases)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

examples/dotnet/Program.cs

@@ -2010,6 +2010,47 @@ namespace test_mapi
             }
         }
 
+        /// <summary>
+        /// Extract unsatisfiable core example with AssertAndTrack
+        /// </summary>
+        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.

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

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);
     }

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.
     */

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;