No effect when asserting background axioms in fixedpoint (spacer) engine

[Majeux]

I am trying to use the fixedpoint (spacer) engine to solve a reachability problem. Each state in the trace should have a constraint on the number of true variables. I mainly use the C++ API, but found the Z3_fixedpoint_assert() function from the C API which should assert "background axioms" for the PDR mode.

But asserting formulas does not seem to have any effect on the result. The same trace is generated every time, which violates the given constraint. The engine has the following settings enabled through the C++ API:

p.set("engine", "spacer");
p.set("spacer.random_seed", 1);
p.set("spacer.push_pob", true);
p.set("spacer.use_bg_invs", true);

The solver is prepared in the following state:

(declare-rel state (Bool Bool Bool Bool Bool))
(declare-rel step (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
(declare-var A Bool)
(declare-var B Bool)
(declare-var C Bool)
(declare-var D Bool)
(declare-var E Bool)
(declare-var F Bool)
(declare-var G Bool)
(declare-var H Bool)
(declare-var I Bool)
(declare-var J Bool)
(assert (forall ((a_1 Bool)
         (b_1 Bool)
         (b_2 Bool)
         (c_1 Bool)
         (c_2 Bool)
         (a_1.p Bool)
         (b_1.p Bool)
         (b_2.p Bool)
         (c_1.p Bool)
         (c_2.p Bool))
  (! ((_ at-most 3) a_1 b_1 b_2 c_1 c_2) :weight 0)))
(rule (! (=> (and (not J) (not I) (not H) (not G) (not F)) (state J I H G F)) :named I))
(rule (! (=> (and (state J I H G F) (step J I H G F E D C B A)) (state E D C B A)) :named ->))
(rule (! (=> true (step J I H G F (not J) I H G F)) :named |flip a_1|))
(rule (! (=> true (step J I H G F J (not I) H G F)) :named |flip b_1|))
(rule (! (=> (and true I F) (step J I H G F J true (not H) G true)) :named |flip b_2|))
(rule (! (=> (and true I) (step J I H G F J true H (not G) F)) :named |flip c_1|))
(rule (! (=> (and true J G) (step J I H G F true I H true (not F))) :named |flip c_2|))

Even when asserting true or false, the result does not change.

...
(declare-var J Bool)
(assert true)
(assert false)
(rule (! (=> (and (not J) (not I) (not H) (not G) (not F)) (state J I H G F)) :named I))
...

Which leaves me wondering if I am using the function correctly, and if I should be using these background assertions at all to constraint the steps. I can achieve the desired behaviour by including the constraint in every rule:

(declare-rel state (Bool Bool Bool Bool Bool))
(declare-rel step (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
(declare-var A Bool)
(declare-var B Bool)
(declare-var C Bool)
(declare-var D Bool)
(declare-var E Bool)
(declare-var F Bool)
(declare-var G Bool)
(declare-var H Bool)
(declare-var I Bool)
(declare-var J Bool)
(rule (! (=> (and (not J) (not I) (not H) (not G) (not F)) (state J I H G F)) :named I))
(rule (! (=> (and (state J I H G F) (step J I H G F E D C B A)) (state E D C B A)) :named ->))
(rule (! (=> ((_ at-most 3) J I H G F) (step J I H G F (not J) I H G F)) :named |flip a_1|))
(rule (! (=> ((_ at-most 3) J I H G F) (step J I H G F J (not I) H G F)) :named |flip b_1|))
(rule (! (=> (and ((_ at-most 3) J I H G F) I F) (step J I H G F J true (not H) G true)) :named |flip b_2|))
(rule (! (=> (and ((_ at-most 3) J I H G F) I) (step J I H G F J true H (not G) F)) :named |flip c_1|))
(rule (! (=> (and ((_ at-most 3) J I H G F) J G) (step J I H G F true I H true (not F))) :named |flip c_2|))

But if there is a build in mechanism for it, that may be more efficient.

In short: should I use the background assertions to constrain each state along a possible trace? If so, how?

[agurfinkel]

Spacer does not support background assertions through this interface. The safest way to use it is to add desired constraints directly in the rules.

Under some conditions, you can inject extra constraints directly into the engine. This is sometimes sound (for example, if constraints are already implied by the rules, but are not explicit in the rules), and sometimes not.

There are two mechanisms to inject constraints:

• Z3_fixedpoint_add_cover injects a fact directly into the lemmas kept by the engine.
• Z3_fixedpoint_add_invariant adds an invariant that is only used during propagate.

We found that injecting too many constraints with add_cover affects generalization, so that is the reason for the second options. These options are not user friendly since they allow injecting info directly into the engine. The user must be careful to not inject something that violates the invariants that the engine maintains.