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
- remove reduce_invertible. It is subsumed by reduce_uncstr(2)
- introduce a simplifier for reduce_unconstrained. It uses reference counting to deal with inefficiency bug of legacy reduce_uncstr. It decomposes theory plugins into expr_inverter.
reduce_invertible is a tactic used in most built-in scenarios. It is useful for removing subterms that can be eliminated using "cheap" quantifier elimination. Specifically variables that occur only once can be removed in many cases by computing an expression that represents the effect computing a value for the eliminated occurrence.
The theory plugins for variable elimination are very partial and should be augmented by extensions, esp. for the case of bit-vectors where the invertibility conditions are thoroughly documented by Niemetz and Preiner.
the solve_eqs_tactic is to be replaced by a re-implementation that uses solve_eqs in the simplifiers directory.
The re-implementation should address efficiency issues with the previous code.
At this point it punts on low level proofs. The plan is to use coarser
dependency tracking instead of low level proofs for pre-processing. Dependencies can be converted into a proof hint representation that can be checked using a stronger checker.
simplifiers layer is a common substrate for global non-incremental and incremental processing.
The first two layers are new, but others are to be ported form tactics.
- bv::slice - rewrites equations to cut-dice-slice bit-vector extractions until they align. It creates opportunities for rewriting portions of bit-vectors to common sub-expressions, including values.
- euf::completion - generalizes the KB simplifcation from asserted formulas to use the E-graph to establish a global and order-independent canonization.
The interface dependent_expr_simplifier is amenable to forming tactics. Plugins for asserted-formulas is also possible but not yet realized.
- ensure mk_extract performs simplification to distribute over extract and removing extract if the range is the entire bit-vector
- ensure bool_rewriter simplifeis disjunctions when applicable.
move self-checking functionality to inside sat/smt so it can be used on-line and not just off-line.
when self-validation fails, use vs, not clause, to check. It allows self-validation without checking and maintaining RUP validation.
new options sat.smt.proof.check_rup, sat.smt.proof.check for online validation.
z3 sat.smt.proof.check=true sat.euf=true /v:1 sat.smt.proof.check_rup=true /st file.smt2 sat.smt.proof=p.smt2
EUF proofs are checked modulo union-find.
Equalities are added to to union-find if they are assumptions or if they can be derived using congruence closure. The congruence closure assumptions are added as proof-hints.
Note that this proof format does not track equality inferences, symmetry and transitivity. Instead they are handled by assuming a union-find based checker.
