PR changes

cvc5_pythonic_api/cvc5_pythonic.py

@@ -6267,8 +6267,6 @@ def setOption(self, name=None, value=None, **kwargs):
             kwargs[name] = value
         for k, v in kwargs.items():
             _assert(isinstance(k, str), "non-string key " + str(k))
-            if k == 'unsat_core':
-                k = 'produce-unsat-cores'
             if isinstance(v, bool):
                 v = "true" if v else "false"
             elif not isinstance(v, str):
@@ -6331,7 +6329,7 @@ def unsat_core(self):
 
         These are the unsat ("failed") assumptions.
 
-        To enable this, set the option "produce-unsat-assumptions" to true. 
+        To enable this, set the option "produce-unsat-assumptions" to true.
 
         >>> a,b,c = Bools('a b c')
         >>> s = Solver()
@@ -6350,7 +6348,7 @@ def unsat_core(self):
         sat
         """
         core = self.solver.getUnsatAssumptions()
-        return [ BoolRef(c) for c in core] 
+        return [BoolRef(c) for c in core]
 
 
 def SolverFor(logic, ctx=None, logFile=None):

test/pgms/unsat_core.py → test/pgms/unsat_assumptions.py

@@ -1,25 +1,31 @@
 from cvc5_pythonic_api import *
-#from z3 import *
 
 
 def reset_solver(s):
     s.reset()
     s.set('produce-unsat-assumptions','true')
 
-def check_unsat_core(assertions, core):
+def validate_unsat_assumptions(assumptions, core):
+    # checks that the produced unsat assumptions (core) match the assumptions (assumptions) sent to the check function
+    return sum([c in assumptions for c in core]) == len(core) 
+
+
+def check_unsat_assumptions(assertions, core):
+    # This function checks wether, given assertions,  the produced unsat assumptions (core) also lead to unsat result
     slvr = Solver()
     slvr.set('produce-unsat-assumptions','true')
     for a in assertions:
         slvr.add(a)
     return s.check(*core) == unsat
 
-nontrivial_counter = 0 
+
+# To make make sure the unsat_core function works there should be at least one nontrivial solution - a solution that doesn't contain all the assumptions sent in the check function.
+nontrivial_counter = 0  
 
 p1, p2, p3 = Bools('p1 p2 p3')
 x, y = Ints('x y')
 s = Solver()
-s.set('produce-unsat-assumptions','true')
-
+reset_solver(s)
 assertions = [Implies(p1, x > 0), Implies(p2, y > x), Implies(p2, y < 1), Implies(p3, y > -3)]
 
 for a in assertions:
@@ -32,8 +38,8 @@ def check_unsat_core(assertions, core):
 core = s.unsat_core()
 
 
-assert sum([c in assumptions for c in core]) == len(core)
-assert check_unsat_core(assertions,core)
+assert validate_unsat_assumptions(assumptions,core)
+assert check_unsat_assumptions(assertions,core)
 if len(core) < len(assumptions):
     nontrivial_counter += 1
 
@@ -56,8 +62,8 @@ def check_unsat_core(assertions, core):
 
 unsat_core = s.unsat_core()
 
-assert sum([c in assumptions for c in unsat_core]) == len(unsat_core)
-assert check_unsat_core(assertions,assumptions)
+assert validate_unsat_assumptions(assumptions,unsat_core) 
+assert check_unsat_assumptions(assertions,assumptions)
 if len(unsat_core) < len(assumptions):
     nontrivial_counter += 1
 
@@ -79,8 +85,8 @@ def check_unsat_core(assertions, core):
 
 unsat_core = s.unsat_core()
 
-assert sum([c in assumptions for c in unsat_core]) == len(unsat_core)
-assert check_unsat_core(assertions,assumptions)
+assert validate_unsat_assumptions(assumptions,unsat_core)
+assert check_unsat_assumptions(assertions,assumptions)
 if len(unsat_core) < len(assumptions):
     nontrivial_counter += 1
 
@@ -104,8 +110,8 @@ def check_unsat_core(assertions, core):
 
 unsat_core = s.unsat_core()
 
-assert sum([c in assumptions for c in unsat_core]) == len(unsat_core)
-assert check_unsat_core(assertions,assumptions)
+assert validate_unsat_assumptions(assumptions,unsat_core)
+assert check_unsat_assumptions(assertions,assumptions)
 if len(unsat_core) < len(assumptions):
     nontrivial_counter += 1
 
@@ -131,8 +137,8 @@ def check_unsat_core(assertions, core):
 
 unsat_core = s.unsat_core()
 
-assert sum([c in [ Length(s2) < 2 ] for c in unsat_core]) == len(unsat_core)
-assert check_unsat_core(assertions,[ Length(s2) < 2 ])
+assert validate_unsat_assumptions([Length(s2) < 2], unsat_core)
+assert check_unsat_assumptions(assertions,[ Length(s2) < 2 ])
 if len(unsat_core) < len([ Length(s2) < 2 ]):
     nontrivial_counter += 1