- 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.
in an iteration of inc-sat-solver introduce sat-smt-solver to allow incremental pre-processing.
The aim is to allow incrementally handling formulas while at the same time retaining the main benefits of global in/pre-processing that change models. Previous incremental solving capabilities have been limited to use pre-processing that does not require model conversion.
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.
- 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.
