It happens sometimes that e.g. the internalizer goes above the soft memory limit
But since it's only by a small amount, when the exception propagates back to the context, some stuff
has been freed already and we are not longer above the memory threshold
Just delete these asserts
* replace u_set by indexed_uint_set
* replace u_set by indexed_uint_set
* create insert-fresh and insert for indexed_uint_set to make use cases with non-fresh inserts easier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* update nightly to pull arm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* update nightly to pull arm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixing the build of lp_tst
* update nightly to pull arm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* replace u_set by indexed_uint_set
* replace u_set by indexed_uint_set
* fixing the build of lp_tst
* remove unnecessery call to contains() before
insert to indexed_uint_set
* formatting, no check for contains()
in indexed_uint_set, always init m_touched_rows to nullptr
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* qe_lite: cleanup and comment
no change to code
* mbp_arrays: refactor out partial equality (peq)
Partial array equality, PEQ, is used as an intermediate
expression during MBP for arrays. We need to factor it out
so that it can be shared between MBP-QEL and existing MBP.
Partial array equality (peq) is used in MBP for arrays.
Factoring this out to be used by multiple MBP implementations.
* rewriter: new rewrite rules
These rules are specializes for terms that are created in QEL.
QEL commit is comming later
* datatype_rw: new rewrite rule for ADTs
The rule handles this special case:
(cons (head x) (tail x)) --> x
* array_rewriter rules for rewriting PEQs
Special rules to simplify PEQs
* th_rewriter: wire PEQ simplifications
* spacer_iuc: avoid terms with default in IUC
Spacer prfers to not have a term representing default value of an array.
This guides IUC from picking such terms in interpolation
* mbp_term_graph: replace root with repr
* mbp_term_graph: formatting
* mbp_term_graph: class_props, getters, setters
Class properties allow to keep information for an equivalence class.
Getters and setters for terms allow accessing information
* mbp_term_graph: auxiliary methods for qel
QEL commit is comming later in the history
* mbp_term_graph: bug fix
* mbp_term_graph: pick, refine repr, compute cgrnd
* mbp_term_graph: internalize deq
* mbp_term_graph: constructor
* mbp_term_graph: optionally internalize equalities
Reperesent equalities explicitly by nodes in the term_graph
* qel
* formatting
* comments on term_lt
* get terms and other api for mbp_qel
* plugins for mbp_qel
* mbp_qel_util: utilities for mbp_qel
* qe_mbp: QEL-based mbp
* qel: expose QEL API
* spacer: replace qe_lite in qe_project_spacer by qel
This changes the default projection engine that spacer uses.
* cmd_context: debug commands for qel and mbp_qel
New commands are
mbp-qel -- MBP with term graphs
qel -- QEL with term graphs
qe-lite -- older qelite
* qe_mbp: model-based rewriters for arrays
* qe_mbp: QEL-based projection functions
* qsat: wire in QEL-based mbp
* qsat: debug code
* qsat: maybe a bug fix
Changed the code to follow the paper by adding all predicates above a given
level, not just predicates of immediately preceding level.
* chore: use new api to create solver in qsat
* mbp_term_graph use all_of idiom
* feat: solver for integer multiplication
* array_peq: formatting, no change to code
* mbp_qel_util: block comment + format
* mbt_term_graph: clang-format
* bug fix. Move dt rewrite to qe_mbp
* array_peq: add header
* run clang format on mbp plugins
* clang format on mul solver
* format do-while
* format
* format do-while
* update release notes
---------
Co-authored-by: hgvk94 <hgvk94@gmail.com>
Co-authored-by: Isabel Garcia <igarciac@uwaterloo.ca>
this will allow copying the solver state within a scope.
The new solver state has its state at level 0. It is not possible to pop scopes from the new solver (you can still pop scopes from the original solver). The reason for this semantics is the relative difficulty of implementing (getting it right) of a state copy that preserves scopes.
remove bv_eq_axioms as an external option to toggle.
Diseqalities have to be enforced for extensionality.
There are no internal code paths where the option is set to false.
An initial update to support polymorphism from SMTLIB3 and the API (so far C, Python).
The WIP SMTLIB3 format is assumed to be supporting the following declaration
```
(declare-type-var A)
```
Whenever A is used in a type signature of a function/constant or bound quantified variable, it is taken to mean that all instantiations of A are included in the signature and assertions.
For example, if the function f is declared with signature A -> A, then there is a version of f for all instances of A.
The semantics of polymorphism appears to follow previous proposals: the instances are effectively different functions.
This may clash with some other notions, such as the type signature forall 'a . 'a -> 'a would be inhabited by a unique function (the identity), while this is not enforced in this version (and hopefully never because it is more busy work).
The C API has the function 'Z3_mk_type_variable' to create a type variable and applying functions modulo polymorphic type signatures is possible.
The kind Z3_TYPE_VAR is added to sort discriminators.
This version is considered as early alpha. It passes a first rudimentary unit test involving quantified axioms, declare-fun, define-fun, and define-fun-rec.
check-assumptions with compound formulas create fresh proxy variables both during compilation to internal format and for the assumptions. These fresh variables may occur in lemmas that are created during search. The lemmas are garbage for future check-sats, but the solver needs to be allowed to invoke GC. Adding a GC call before a check-sat with assumptions allows removing some lemmas every time a new assumptions are used. Eager GC when using assumptions is used elsewhere, for example in cube&conquer scenarios where lemmas learned from one set of assumptions are less likely to be useful for other assumptions.
With the GC invocation memory grows at a lesser pace. However, it is not entirely free of memory increases. To avoid memory bloat, have the solver pre-compile the assumptions by defining them as propositional variables, add assertions that the propositional variables are equivalent to the compound formulas and use the propositional variables as assumptions. The same propositional variables come with no extra overhead when invoking check-assumptions. The lemmas are then over the same fixed vocabulary. It is generally a good idea to recycle useful lemmas during the enumeration pass.
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.
- scan_for_linear returns true if it finds a new linear equation. It then should break GB.
- if scan_for_linear returns false, it should still allow try_modify_eqs.
This behavior was masked by requiring scan_for_linear to always be true before
allowing try_to_modify_eqs.
based on repro from Guido Martinez @mtzguido
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
- add check for lambdas similar to as-array in context of quantifiers. MBQI is not a decision procedure for this combination and can then incorrectly conclude satisfiabiltiy.
Scenario
The formula contains assertions
- bv = (map or (lambda ..) t)
- forall y (not (select bv (pair s y)))
Since bv is extensionally equal to a term that depends on a lambda, MBQI cannot just take the current finite approximation of bv when checking the quantifier for satisfiability.
this update enables new incremental linear axioms based on division terms.
It also consolidates some of the backtracking state in nla_core / emons to use stack traces instead of custom backtracking state.
- 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.
-
- 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.
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))
```
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.
log theory propagations with annotation "smt".
It allows tracking theory propagations (when used in conflicts) in the clause logs similar to the new core.
So far the format is
(forall ((x Int)) body) (not (body[t/x]))
The alternative could be the clause
(not (forall ((x Int)) body)) body[t/x]
they just better be consistent between engines
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically
* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation
The bug was that axiom generation was not enabled on last_index, so no axioms got created to constrain last-index.
With default settings the solver is now very slow on this example. It is related to that the smallest size of a satisfying assignment is above 24. Pending a good heuristic to find initial seeds and increments for iterative deepening, I am adding another parameter smt.seq.min_unfolding that when set to 30 helps for this example.
Occurrences of map and fold are interpreted.
They are defined when the seq argument is expanded into a finite
concatenation. The ensure this expansion takes place, each fold/map term
is registered and defined through rewrites when the seq argument simplifies.
* Make spacer_sem_matcher::reset() public
* Add .clang-format for src/muz/spacer
* Mark substitution::get_bindings() as const
* Fix in spacer_antiunify
* Various helper methods in spacer_util
Minor functions to compute number of free variables, detect presence of certain
sub-expressions, etc.
The diff is ugly because of clang-format
* Add spacer_cluster for clustering lemmas
A cluster of lemmas is a set of lemmas that are all instances of the same
pattern, where a pattern is a qff formula with free variables.
Currently, the instances are required to be explicit, that is, they are all
obtained by substituting concrete values (i.e., numbers) for free variables of
the pattern.
Lemmas are clustered in cluster_db in each predicate transformer.
* Integrate spacer_cluster into spacer_context
* Custom clang-format pragmas for spacer_context
spacer_context.(cpp|h) are large and have inconsistent formatting. Disable
clang-format for them until merge with main z3 branch and re-format.
* Computation of convex closure and matrix kernel
Various LA functions. The implementations are somewhat preliminary.
Convex closure is simplemented via syntactic convex closure procedure.
Kernel computation considers many common cases.
spacer_arith_kernel_sage implements kernel computation by call external
Sage binary. It is used only for debugging and experiments. There is no
link dependence on Sage. If desired, it can be removed.
* Add spacer_concretize
* Utility methods for spacer conjecture rule
* Add spacer_expand_bnd_generalizer
Generalizes arithmetic inequality literals of the form x <= c,
by changing constant c to other constants found in the problem.
* Add spacer_global_generalizer
Global generalizer checks every new lemma against a cluster
of previously learned lemmas, and, if possible, conjectures
a new pob, that, when blocked, generalizes multiple existing
lemmas.
* Remove fp.spacer.print_json option
The option is used to dump state of spacer into json for debugging.
It has been replaced by `fp.spacer.trace_file` that allows dumping an execution
of spacer. The json file can be reconstructed from the trace file elsewhere.
* Workaround for segfault in spacer_proof_utils
Issue #3 in hgvk94/z3
Segfault in some proof reduction. Avoid by bailing out on reduction.
* Revert bug for incomplete models
* Use local fresh variables in spacer_global_generalizer
* Cleanup of spacer_convex_closure
* Allow arbitrary expressions to name cols in convex_closure
* WIP: convex closure
* WIP: convex closure
* Fix bindings order in spacer_global_generalizer
The matcher creates substitution using std_order, which is
reverse of expected order (variable 0 is last). Adjust the code
appropriately for that.
* Increase verbosity level for smt_context stats
* Dead code in qe_mbp
* bug fixes in spacer_global_generalizer::subsumer
* Partially remove dependence of size of m_alphas
I want m_alphas to potentially be greater than currently used alpha variables.
This is helpful for reusing them across multiple calls to convex closure
* Subtle bug in kernel computation
Coefficient was being passed by reference and, therefore, was
being changed indirectly.
In the process, updated the code to be more generic to avoid rational
computation in the middle of matrix manipulation.
* another test for sparse_matrix_ops::kernel
* Implementation of matrix kernel using Fraction Free Elimination
Ensures that the kernel is int for int matrices. All divisions are exact.
* clang-format sparse_matrix_ops.h
* another implementation of ffe kernel in sparse_matrix_ops
* Re-do arith_kernel and convex_closure
* update spacer_global_generalization for new subsumer
* remove spacer.gg.use_sage parameter
* cleanup of spacer_global_generalizer
* Removed dependency on sage
* fix in spacer_convex_closure
* spacer_sem_matcher: consider an additional semantic matching
disabled until it is shown useful
* spacer_global_generalizer: improve do_conjecture
- if conjecture does not apply to pob, use lemma instead
- better normalization
- improve debug prints
* spacer_conjecture: formatting
* spacer_cluster: improve debug prints
* spacer_context: improve debug prints
* spacer_context: re-queue may pobs
enabled even if global re-queue is disabled
* spacer_cluster print formatting
* reset methods on pob
* cleanup of print and local variable names
* formatting
* reset generalization data once it has been used
* refactored extra pob creation during global guidance
* fix bug copying sparse matrix into spacer matrix
* bug fix in spacer_convex_closure
* formatting change in spacer_context
* spacer_cluster: get_min_lvl
chose level based on pob as well as lemmas
* spacer_context: add desired_level to pob
desired_level indicates at which level pob should be proved.
A pob will be pushed to desired_level if necessary
* spacer_context: renamed subsume stats
the name of success/failed was switched
* spacer_convex_closure: fix prototype of is_congruent_mod()
* spacer_convex_closure: hacks in infer_div_pred()
* spacer_util: do not expand literals with mod
By default, equality literal t=p is expanded into t<=p && t>=p
Disable the expansion in case t contains 'mod' operator since such
expansion is usually not helpful for divisibility
* spacer_util: rename m_util into m_arith
* spacer_util: cleanup normalize()
* spacer_util: formatting
* spacer_context: formatting cleanup on subsume and conjecture
* spacer_context: fix handling may pobs when abs_weakness is enabled
A pob might be undef, so weakness must be bumped up
* spacer_arith_kernel: enhance debug print
* spacer_global_generalizer: improve matching on conjecture
* spacer_global_generalizer: set desired level on conjecture pob
* spacer_global_generalizer: debug print
* spacer_global_generalizer: set min level on new pobs
the new level should not be higher than the pob that was generalized
* spacer_global_generalizer: do no re-create closed pobs
If a generalized pob exist and closed, do not re-create it.
* spacer_context: normalize twice
* spacer_context: forward propagate only same kind of pobs
* sketch of inductive generalizer
A better implementation of inductive generalizer that in addition to dropping
literals also attempts to weaken them.
Current implementation is a sketch to be extended based on examples/requirements.
* fix ordering in spacer_cluster_util
* fix resetting of substitution matcher in spacer_conjecture
Old code would forget to reset the substitution provided to the sem_matcher.
Thus, if the substitution was matched once (i.e., one literal of interest is
found), no other literal would be matched.
* add spacer_util is_normalized() method
used for debugging only
* simplify normalization of pob expressions
pob expressions are normalized to increase syntactic matching.
Some of the normalization rules seem out of place, so removing them for now.
* fix in spacer_global_generalizer
If conjecture fails, do not try other generalization strategies -- they will not apply.
* fix in spacer_context
do not check that may pob is blocked by existing lemmas.
It is likely to be blocked. Our goal is to block it again and generalize
to a new lemma.
This can be further improved by moving directly to generalization when pob is
blocked by existing lemmas...
Co-authored-by: hgvk94 <hgvk94@gmail.com>
this update addresses some perf regressions introduced when handling axioms for bv2int and a memory smash regression when decoupling bv-ackerman from in-processing. It adds a filter based on bv_eq_axioms for disabling ackerman reductions on disequalities.
floating points may also track bit-literals.
Since the legacy solver doesn't handle dual tracking of literals we just let the floating point solver track.
- add option smt.bv.reduce_size.
- it allows to apply incremental pre-processing of bit-vectors by identifying ranges that are known to be constant.
This rewrite is beneficial, for instance, when bit-vectors are constrained to have many high-level bits set to 0.
- add solver.axioms2files
- prints negated theory axioms to files. Each file should be unsat
- add solver.lemmas2console
- prints lemmas to the console.
- remove option smt.arith.dump_lemmas. It is replaced by solver.axioms2files
This update allows the python bindings for user-propagator to handle functions that are declared to be registered with the user propagator plugin. It fixes a bug in UserPropagateBase.add to allow registering terms dynamically during search.
It also fixes a bug in theory_user_propagate as scopes were not fully pushed when the solver gets the callbacks for new equalities and new disequalities.
It also adds equality and disequality interfaces to the sat/smt solver version (which isn't being exercised in earnest yet)
* Added function to select the next variable to split on
* Fixed typo
* Small fixes
* uint -> int
* Fixed missing assignment for binary clauses
* Added missing decide-callback for tactics
this update integrates inferences to smt.arith.solver=6 related to grobner basis computation and handling of div/mod axioms to reconcile performance with smt.arith.solver=2.
The default of smt.arth.nl.grobner_subs_fixed is changed to 1 to make comparison with solver=2 more direct.
The selection of cluster equalities for solver=6 was reconciled with how it is done for solver=2.
expression pointers were changed within a function, but not pinned. So the pointers got stale. To enforce their life-time within the function body (for use in logging) pin the expressions.
recfun decl plugin does not get copied so recursive functions are lost when cloning.
Fix is risky and use case is limited to threads + recursive definitions
An argument to a recursive function would escape the scope of the function application when the recursive function definitions are unfolded. Therefore, such argument occurrences need not be considered for extensional equality / equality sharing.
This filter is mostly relevant for recursive functions that take a lambda expression as argument. Lambda expressions / arrays that occur in shared occurrences are checked for extensionality.
add API to define forward reference to recursively defined datatype.
The forward reference should be used only when passed to constructor declarations that are used in a datatype definition (Z3_mk_datatypes). The call to Z3_mk_datatypes ensures that the forward reference can be resolved with respect to constructors.
* Fixed registering expressions in push/pop
* Reused existing function
* Reverted reusing can_propagate
* Added decide-callback to user-propagator
* Refactoring
* Fixed index
* Added bit2bool to the API
Fixed bug in user-propagator's decide callback
* Fixed typo
