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.
* 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
#6319 - fix incompleteness in propagation of default to all array terms in the equivalence class.
Fix bug with q_mbi where domain restrictions are not using values because the current model does not evaluate certain bound variables to values. Set model completion when adding these bound variables to the model to ensure their values are not missed.
Add better propagation of diagnostics when tactics and the new solver return unknown. The reason for unknown can now be traced to what theory was culprit (currently no additional information)
using a queue for disequality propagaiton was a regression: values of numerals can change along the same stack so prior passing the filter does not mean it passes later.
conversion from AIG to expressions should always use the optimized conversion function.
the aig-tactic should throttle regarding output bloat from AIG.
If the expression after AIG simpification, for whatever reason, is bloated the rewrite does not take place.
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically
* Dotnet Api: suppress GC finalization of dotnet context in favor of re-registering finalization
* Dotnet Api: enable concurrent dec-ref even if context is created without parameters.
* Dotnet Api: removed dead code.
literals that are replayed need to be registered with respective theories, otherwise, they will not propagate with the theories (the enode have to be attached with relevant theory variables).
delay propagation on each disequality/equality should suffice once. It adds relevant inequalities to ensure the arithmetic solver is coherent about disequalities.
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.
The notion of reference counted contexts never worked.
The reference count to a context only ends up being 0 if the GC kicks in and disposes the various z3 objects. A call to Dispose on Context should free up all resources associated with that context. In exchange none of the resources are allowed any other operation than DecRef. The invocations of DecRef are protected by a lock and test on the context that the native pointer associated with the context is non-zero. Dispose sets the native pointer to zero.
Z3_enable_concurrent_dec_ref ensures that:
- calls to decref are thread safe. Other threads can operate on the context without interference.
The Z3_context ensures that
- z3objects allocated, but not disposed during the lifetime of Z3_context are freed when Z3_context is deleted (it triggers a debug warning, but this is now benign).
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.
The literal "emp" can be true in the current assignment, in which case the clause
cnt or emp or ~postf is true and does not contribute to propagation.
This saves, potentially, for generating lemmas for postf.
Add a lemma a = "" or |s| >= idx when a = tail(s, idx)
The lemma ensures that length bounding on s is enforced
(the branch that expands not-contains for long sequences s is closed).
* 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>
Conditionals are used to guard unfolding of recursive functions.
This is, as shown in #6304, incompatible with the case where recursive functions are used inside if-then-else guards.
We address this by disabling if-conditions as guards if they contain a recursive definition.
The approach is simplistic: if a recursive function, defined prior (not mutually recursive) is used in a guard it should be fine and the condition can guard the current recursive unfolding.
crash due to not checking for dead rows.
non-termination due to solving div and mod separately.
To ensure termination one needs to at least process them simultaneously, otherwise the metric of number-of-terms x under number of mod/div does not decrease. Substituting in K*y + z under either a mod or div increases the number of terms under a mod/div when eliminating only one of the kinds.
Currently handling divides constraints separately because pre-existing solution uses the model to determine z as a constant between 0 and K-1. The treatment of mod/div is supposed to be more general and use a variable while at the same time reducing the mod/div terms where the eliminated variable is used (the variable z is not added under the mod/div terms, but instead the model is used to determine cut-offs to calculate mod/div directly.
The existing comment describes macros as "formulas of the form
`(forall X (= (f X) T[X]))` ... where `T[X]` does not contain `X`". This is
incorrect; of course the macros' definitions are allowed to be in terms of
the macros' arguments. The comment should say "...does not contain `f`" because
macros can't be recursive.
This commit overhauls the proof format (in development) for the new core.
NOTE: this functionality is work in progress with a long way to go.
It is shielded by the sat.euf option, which is off by default and in pre-release state.
It is too early to fuzz or use it. It is pushed into master to shed light on road-map for certifying inferences of sat.euf.
It retires the ad-hoc extension of DRUP used by the SAT solver.
Instead it relies on SMT with ad-hoc extensions for proof terms.
It adds the following commands (consumed by proof_cmds.cpp):
- assume - for input clauses
- learn - when a clause is learned (or redundant clause is added)
- del - when a clause is deleted.
The commands take a list of expressions of type Bool and the
last argument can optionally be of type Proof.
When the last argument is of type Proof it is provided as a hint
to justify the learned clause.
Proof hints can be checked using a self-contained proof
checker. The sat/smt/euf_proof_checker.h class provides
a plugin dispatcher for checkers.
It is instantiated with a checker for arithmetic lemmas,
so far for Farkas proofs.
Use example:
```
(set-option :sat.euf true)
(set-option :tactic.default_tactic smt)
(set-option :sat.smt.proof f.proof)
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const u Int)
(assert (< x y))
(assert (< y z))
(assert (< z x))
(check-sat)
```
Run z3 on a file with above content.
Then run z3 on f.proof
```
(verified-smt)
(verified-smt)
(verified-smt)
(verified-farkas)
(verified-smt)
```
a recent opened and closed bug report was due to an error of taking bit-wise or between two bit-vectors of different size. The error message was not understood by the user. Adding a little extra generic information to see if it helps.
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.
previous scheme has Ackmerman module instrument main solver to backjump and simplify when reaching a threshold.
This destroys overall performance: simplification does many more things than invoking Ackerman axioms.
Having a dependency between simplification (in-processing) and depleting a priority queue of auxiliary axioms therefore hurts overall performance. It has to be decoupled. The current approach is now to empty the axiom queue on occasion.
It is still not ideal - it should be coupled with the search level - axioms don't survive higher levels where redundant clauses get garbage collected as they don't have a chance of being used.
- 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.
elimination of mod/div should be applied to all occurrences of x under mod/div at the same time. It affects performance and termination to perform elimination on each occurrence since substituting in two new variables for eliminated x doubles the number of variables under other occurrences.
Also generalize inequality resolution to use div.
The new features are still disabled.
This update changes the handling of mod and adds support for nested div terms.
Simple use cases that are handled using small results are given below.
```
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (exists ((x Int)) (and (<= y (* 10 x)) (<= (* 10 x) z))))
(apply qe2)
(reset)
(declare-const y Int)
(assert (exists ((x Int)) (and (> x 0) (= (div x 41) y))))
(apply qe2)
(reset)
(declare-const y Int)
(assert (exists ((x Int)) (= (mod x 41) y)))
(apply qe2)
(reset)
```
The main idea is to introduce definition rows for mod/div terms.
Elimination of variables under mod/div is defined by rewriting the variable to multiples of the mod/divisior and remainder.
The functionality is disabled in this push.
- 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
Commit #b361226 changed symbol visibility from a global to a local option.
This creates inconsistency for shell that is compiled as an executable rather
than as z3 component.
This commit adds same local options to shell target in cmake.
Prior to the fix, clang on OSX complains with lots of warnings about symbol visibility
being different in different translation units that are linked together
This was only being enabled on Windows, Linux, and FreeBSD. (FreeBSD
only had it enabled in the legacy build system, not in cmake.)
`thread_local` is part of C++11, so now that we require C++17
or later and more recent compilers, this should work everywhere
that threading does, so only disable it within a `SINGLE_THREAD`
build.
Previously, we were only using std::hexfloat on Windows on VS2013
and later.
Since std::hexfloat is part of C++11 and we require C++11 to build
the Z3 library, this should be supported everywhere.
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
Add Z3_enable_concurrent_dec_ref to the API.
It is enables behavior of dec_ref functions that are exposed over the API to work with concurrent GC. The API calls to dec_ref are queued and processed in the main thread where context operations take place (in a way that is assumed thread safe as context operations are only allowed to be serialized on one thread at a time).
The idea is to set _concurrent_dec_ref from the API
(function not yet provided externally, but you can experiment with it by setting the default of m_concurrent_dec_ref to true).
It then provides concurrency support for dec_ref operations.
