1

my question is that i do not see that the unsat_core tracks any assertions that are provided in an entire chunk using the api 

f = Z3_parse_smtlib2_string(c, "unsat_core_example1.smt2",0,0,0,0,0,0);
params p(c);
p.set(":unsat-core", true);
s.set(p);
// enabling unsat core tracking
expr r = to_expr(c, f);

unsat_core_example1.smt2:

(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
(declare-fun s () Bool)
(assert (! (or p q) :named a1))
(assert (! (implies r s) :named a2))
(assert (! (implies s (iff q r)) :named a3))
(assert (! (or r p) :named a4))
(assert (! (or r s) :named a5))
(assert (! (not (and r q)) :named a6))
(assert (! (not (and s p)) :named a7))

it seems like the annotation :named is not being processed, as the unsat_core vector returned is always empty.

However, this is not the case if i were to use z3.exe and input the file in.

Any idea what could be the cause?

user3522920
  • 11
  • 1

1 Answers1

2

The Z3_parse_smtlib2_file function does not support all of SMTLIB2, it's really just a convenience function; it's output is not guaranteed to completely cover all of the language (e.g., it doesn't execute commands like check-sat or some set-option commands). It was also written as an extension of a previous SMTLIB1 parser which was written long before the goal/tactic/solver architecture was introduced and consequently not all information is carried over to this new architecture.

In this particular case, the assertion names are indeed saved inside the context, but Z3_parse_smtlib2_file does not return a set of assertions and names; it returns a single expression which is unnamed. To accurately represent an SMTLIB2 benchmark the signature of the function would have to change significantly.

In the example given, the expression which is asserted into the solver is r, i.e., we would have something like

s.add(r);

this essentially asks the solver the assert the unnamed assertion r, but there is no support for "subnames" for expressions inside of r. We can still name r itself however, e.g., by calling

s.add(r, "top")

which results in the correct unsat core.

Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • hi, christoph, thanks for the reply, any idea if there are plans for this feature to be implemented? – user3522920 Apr 14 '14 at 01:18
  • There are currently no plans to extend the parser. The preferred way of generating unsat cores is via explicit definition of Boolean constants (see e.g., here: http://stackoverflow.com/questions/8439556/soft-hard-constraints-in-z3) which is more flexible than using the :named annotation. – Christoph Wintersteiger Apr 14 '14 at 10:02