After introducing the rewriter.sort_disjunctions option (#6774), I
noticed a segfault in a Z3 run that was working fine for me before the
PR.
I traced the difference to a slight discrepancy between the first patch
I submitted and the one we ended up merging: my first version would skip
sorting the disjuncts in mk_nflat_core, but still return BR_DONE, while
the patch in master returns BR_FAILED instead.
This patch fixes that problem, and it makes slightly more sense to me to
return a BR_DONE since, if `s` is true, some disjunct (e.g. a `false`
or a repeat) might have been simplified away. However I don't fully
understand this code.
... and I can't say I understand why the segfault happens. Perhaps that
is a separate issue?
This is the file to reproduce:
https://gist.github.com/mtzguido/b7360c74d3d2e42d89f1bd9149ad26f6
Here's a stack trace of the failure, mk_nflat_or_core is not involved.
```
(gdb) where
#0 0x0000555555b98497 in smt::context::get_lit_assignment(unsigned int) const ()
#1 0x0000555555b984cb in smt::context::get_assignment(sat::literal) const ()
#2 0x0000555555b98504 in smt::context::get_assignment(unsigned int) const ()
#3 0x0000555555ca83b8 in smt::context::get_assignment_core(expr*) const ()
#4 0x0000555555c9af5a in smt::context::get_assignment(expr*) const ()
#5 0x0000555555d7bd1d in (anonymous namespace)::has_child_assigned_to(smt::context&, app*, lbool, expr*&, unsigned int) ()
#6 0x0000555555d7c413 in (anonymous namespace)::rel_case_split_queue::next_case_split_core(ptr_vector<expr>&, unsigned int&, unsigned int&, lbool&) ()
#7 0x0000555555d7c589 in (anonymous namespace)::rel_case_split_queue::next_case_split(unsigned int&, lbool&) ()
#8 0x0000555555c9c1b7 in smt::context::decide() ()
#9 0x0000555555ca39fd in smt::context::bounded_search() ()
#10 0x0000555555ca30c2 in smt::context::search() ()
#11 0x0000555555ca273d in smt::context::check(unsigned int, expr* const*, bool) ()
#12 0x0000555555cb166a in smt::kernel::check(unsigned int, expr* const*) ()
#13 0x0000555555cb9695 in (anonymous namespace)::smt_solver::check_sat_core2(unsigned int, expr* const*) ()
#14 0x00005555560dc0c6 in solver_na2as::check_sat_core(unsigned int, expr* const*) ()
#15 0x00005555560d73f3 in combined_solver::check_sat_core(unsigned int, expr* const*) ()
#16 0x00005555560d34e3 in solver::check_sat(unsigned int, expr* const*) ()
#17 0x0000555556097b26 in cmd_context::check_sat(unsigned int, expr* const*) ()
#18 0x0000555556082ff0 in smt2::parser::parse_check_sat() ()
#19 0x0000555556084dc0 in smt2::parser::parse_cmd() ()
#20 0x00005555560861b6 in smt2::parser::operator()() ()
#21 0x00005555560757e6 in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&, char const*) ()
#22 0x00005555555e8f68 in read_smtlib2_commands(char const*) ()
#23 0x00005555555ee6f6 in main ()
(gdb)
```
* patterns: add option for pattern decomposition (pi.decompose_patterns)
True by default, retaining current behavior.
* rewriter: add option for sorting of disjunctions (rewriter.sort_disjunctions)
True by default, retaining current behavior.
destructive equality resolution uses an occurs check function that is only safe for quantifier-free formulas. In the special case where a bound variable is Boolean and occurs on a side of an equality the other side cannot have a quantifier.
* Logical names for function declarations in c++
Currently, for example, the function declaration symbol member for
checking whether multiplication *does not* overflow is called
`m_bv_smul_ovfl`. Since we are introducing the upcoming smtlib2 symbols
that check that multpliciation *does* overflow, the not overflow check
symbols are renamed to `m_bv_smul_no_ovfl` etc.
* Implement smtlib overflow preds for multiplication
Smtlib2 is being extended to include overflow predicates for bit
vectors (see https://groups.google.com/u/1/g/smt-lib/c/J4D99wT0aKI).
This commit introduces the predicates `bvumulo` and `bvsmulo` that
return `true` if the unsigned multiplication overflows or the signed
multiplication underflows or overflows, respectively.
* Move mul overflow predicates to BV logic
* Add a todo on illogical argument order
* Implement mk_unary_pred for bv
* Implement bvnego
* Implement bvuaddo
* Implement bvsaddo
* Implement bvusubo
* Implement bvssubo
* Implement bvsdivo
deals with fluke regression for F* reported by Guido Martinez
Background:
The automatic pattern inference facility looks for terms that contains all bound variables of a quantifier. It may end up with a term that contains all bound variables but the extracted term can be simplified.
Example. The pattern
(ApplyTT (ApplyTT @x3!1 (ApplyTT @x4!0 (:var 1))) (ApplyTT @x4!0 (:var 0)))
can be decomposed into a multi-pattern
(ApplyTT @x4!0 (:var 1))) (ApplyTT @x4!0 (:var 0))
The multi-pattern may enable a quantifier instantiation while the original pattern does not. The multi-pattern should be preferred.
The regression showed up based on a change that should not be considered harmful but turned out to be noticeable.
The change was a simplification of and-or expressions based on sorting. This played with the case split queue used by F* (smt.case_split = 3) that uses a top-level case split of clauses to avoid redundant branches. The net effect was that without sorting, the benchmarks would always choose the opportune branch that enabled matching against the larger term. With sorting it would mostly choose inopportune branches.
- add option pp.no_lets (default = false) to print formulas without let (used by the low-level SMT2 printer).
- print lemmas2console faster by using the low level printer
- enforce elim-and in bool-rewriter when invoking hoisting.
- make cnf tactic more resilient to non-normalized input.
- enable eliminate predicates on ground formulas
- the literal false should not appear in clauses
- the literal true forces a tautology
- fix early return in is_cnf check. It should check all clauses for nested Booleans.
Add the ability to customize incremental pre-processing simplification for the SMTLIB2 front-end. The main new capability is to use pre-processing tactics in incremental mode that were previously not available. The main new capabilities are
- solve-eqs
- reduce-args
- elim-unconstrained
There are several more. Documentation and exposed simplifiers are populated incrementally. The current set of supported simplifiers can be inspected by using z3 with the --simplifiers flag or referring to https://microsoft.github.io/z3guide/docs/strategies/simplifiers
Some pending features are:
- add the ability to update parameters to simplifiers similar to how tactics can be controlled using parameters.
- expose simplification solvers over the binary API.
move sat_smt_preprocess to solver
fix bugs in model_reconstruction_trail for dependency replay
This is a preparatory step for exposing pre-processing as tactics.
- convert reduce-args to a simplifier. Currently exposed as reduce-args2 tactic until the old tactic code gets removed.
- bug fixes in model_reconstruction trail
- allow multiple defs to be added with same pool of removed formulas
- fix tracking of function symbols instead of expressions to filter replay
- add nla_divisions to track (cheap) divisibility lemmas.
-
leverage interval propagation for bounds.
merge functionality with propagate-ineqs tactic
remove the new propagate-bounds tactic and instead use propagate-ineqs
- increase build version to 4.12.1. This prepares updated release for MacOs-11 build on x86
- move literal propagation mode in euf-egraph to a callback and traversal of equivalence class. Track antecedent by newest equality instead of root. This makes equality propagation to literals have similar behavior as in legacy solver and appears to result in a speedup (10% fewer conflicts on QF_UF/QG-classification/qg5/iso_icl478.smt2 in preliminary testing)
- fix interaction of pre-processing and assumptions. Pre-processing has to freeze assumption literals so they don't get eliminated. This is similar to dependencies that are already frozen.
* Add rewrite for array selects of chain of stores of a same value
Example:
```smt
(declare-fun mem () (Array (_ BitVec 4) (_ BitVec 4)))
(declare-const x (_ BitVec 4))
(declare-const y (_ BitVec 4))
; simplifies to #x1
(simplify (select (store (store (store mem #x1 #x1) y #x1) x #x1) #x1))
```
* Update array_rewriter.cpp
* Update array_rewriter.cpp
This update includes an experimental feature to access a congruence closure data-structure after search.
It comes with several caveats as pre-processing is free to eliminate terms. It is therefore necessary to use a solver that does not eliminate the terms you want to track for congruence of. This is partially addressed by using SimpleSolver or incremental mode solving.
```python
from z3 import *
s = SimpleSolver()
x, y, z = Ints('x y z')
s.add(x == y)
s.add(y == z)
s.check()
print(s.root(x), s.root(y), s.root(z))
print(s.next(x), s.next(y), s.next(z))
```
This would crash before:
(declare-fun x () (_ BitVec 4))
(assert (not (bvule x #x1)))
(apply elim-uncnstr2)
That's because the index_set iterator was querying qtail to compute the end of the iteration
But the problem is that elim-uncnstr2 may add new fmls to the goal, as in this case.
The bvule is replaced with an 'or', but since it's negated, it turns into 2 goals
Solve the issue by freezing the qtail for the iteration loop.
This is the right behavior for elim-uncnstr2, as it can't rewrite exprs that haven't been analyzed before
@NikolajBjorner please check if this the right behavior for the other simplifiers. Thank you
- enable sat.smt in smt_tactic that
is invoked by default on first goals
add flatten-clauses
add push-ite
have tptp5 front-end pretty print SMT2 formulas a little nicer.
rename size() to qtail() and introduce shortcuts
ensure tactic goals are not updated if they are in inconsistent state (because indices could be invalidated)
- add sat.smt option to enable the new incremental core (it is not ready for mainstream consumption as cloning and other features are not implemented and it hasn't been tested in any detail yet).
- move "name" into attribute on simplifier so it can be reused for diagnostics by the seq-simplifier.
other updates:
- change signature of advance_qhead to simplify call sites
- have model reconstruction replay work on a tail of dependent_expr state, while adding formulas to the tail.
inc_sat_solver uses bit-blaster, card2bv and max_bv_sharing.
By turning these into simplifiers it will be possible to remove
dependencies on tactics and goals in inc_sat_simplifier and instead use a modular and general incremental pre-processing infrastructure.
literals true/false are not necessarily created when the merge flag is set.
Also disable merge_tf for if-then-else expressions
Perhaps even not insert children of if expressions into congruence table?
perf fix for propagation behavior for equalities in the new core.
The old behavior was not to allow congruence closure on equalities.
The new behavior is to just not allow merging tf with equalities unless they appear somewhere in a foreign context (not under a Boolean operator)
The change re-surfaces merge_tf and enable_cgc distinction from the old core.
They can both be turned on or off.
merge_enabled renamed to cgc_enabled
The change is highly likely to introduce regressions in the new core.
Change propagation of literals from congruence:
- track antecedent enode. There are four ways to propagate
literals from the egraph.
- the literal is an equality and the two arguments are congruent
- the antecedent is merged with node n and the antecedent has a Boolean variable assignment.
- the antecedent is true or false, they are merged.
- the merge_tf flag is toggled to true but the node n has not been merged with true/false
