Jakob Rath
8249a075e1
repropagate outside pop_levels
2023-03-02 15:52:58 +01:00
Jakob Rath
f6b8c8da21
disable replay
2023-03-02 12:24:26 +01:00
Nikolaj Bjorner
aa75ba8a6b
remove parenthesis
2023-03-01 21:03:41 -08:00
Nikolaj Bjorner
fd97be0e3e
move sat.smt.proof.check_rup into solver.proof.check_rup #6616
2023-03-01 21:03:27 -08:00
Nikolaj Bjorner
94b79eefea
add back max_occs parameter dependency to solve-eqs
2023-03-01 20:40:22 -08:00
Nikolaj Bjorner
acd2eaa390
add (disabled) code path to enable nested conjunctions
...
for experiments with disabling flat-and-or dependency
2023-03-01 20:39:39 -08:00
Nikolaj Bjorner
46d37b6e30
fix #6615
...
make rewriting exception safe (for cancelation).
The state during restart in smt_context is not exception safe.
2023-03-01 17:30:07 -08:00
Nikolaj Bjorner
027770930e
fix bug in quasi macro identification: require quantifiers
2023-03-01 17:03:15 -08:00
Nikolaj Bjorner
25d45a3500
fixes and tests for arith-sls
2023-02-28 17:40:09 -08:00
Nikolaj Bjorner
e87fa1c299
remove stale file
2023-02-28 17:40:08 -08:00
Nikolaj Bjorner
79d47eb302
add preprocessor parameter whether to use bound simplifier
2023-02-28 17:40:08 -08:00
Nikolaj Bjorner
76aad689c6
Update smt_context_pp.cpp
...
print units in statistics
2023-02-28 17:40:08 -08:00
Nikolaj Bjorner
5974a2dc58
remove m_b from lar_core_solver
...
the column vector is pure overhead for the way the lar solver uses lp.
Some other solver modules use column vectors b and integrate with the lp_core_solver_base. The interaction model should be reviewed.
Unused solvers should be removed to make it easier to maintain this code.
2023-02-28 17:40:08 -08:00
Kevin Phoenix
1a9990a92f
Use sys.getdefaultencoding() instead of sys.stdout.encoding ( #6612 )
2023-02-28 11:46:10 -08:00
Julian Parsert
6e7d80633d
Documentation on how to add z3 to CMake project using FetchContent and documentation to recdef function. ( #6613 )
...
* Added overloaded versions of context::recfun in the c++ api that allow for the declaration of recursive functions where the domain is given by a z3::sort_vector instead of an arity and sort*
* added documentation to recdef function
* added a section in the README-CMake.md that explains how z3 can be added to a CMake project as a dependency
---------
Co-authored-by: Julian Parsert <julian.parsert@uibk.ac.at>
2023-02-28 11:44:21 -08:00
Nikolaj Bjorner
6450ad82f4
fixup proof logging
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-27 14:46:26 -08:00
Clemens Eisenhofer
4cf24fb5fc
Weaken precondition for overflow narrow
2023-02-25 14:51:26 +01:00
Nikolaj Bjorner
8be6dcce31
finish adding eqs to bv_solver justifications
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-24 10:21:56 -08:00
Arie Gurfinkel
358caa85e2
Merge pull request #6608 from hgvk94/bugfix
...
fix #6543 . don't assume order on bindings
2023-02-24 10:23:57 -05:00
Jakob Rath
5e95a226c5
easy AND for size 1
2023-02-24 13:52:52 +01:00
Jakob Rath
133661d81b
guard pdd-AND against wrong semantics
2023-02-24 13:51:37 +01:00
Jakob Rath
ae8075e22d
check and fix pdd manager confusion
2023-02-24 13:29:59 +01:00
Nikolaj Bjorner
706d542eeb
add propagation justification to bv antecedents
2023-02-23 17:52:34 -08:00
hgvk94
828fff9684
fix #6543 . don't assume order on bindings
2023-02-23 17:35:55 -05:00
Jakob Rath
9b274f349b
potential generalization
2023-02-23 11:24:32 +01:00
Jakob Rath
645f4620de
catch default case
2023-02-23 10:56:12 +01:00
Jakob Rath
5ffd00073a
Enable more general ule simplification ule; flip order
2023-02-22 16:47:14 +01:00
Jakob Rath
6eb0d91504
Tweak ule simplifications
2023-02-22 16:36:10 +01:00
Jakob Rath
14b2c38e7f
Add lemma try_umul_ovfl_noovfl for bench23
2023-02-22 16:32:51 +01:00
Jakob Rath
a8bfd01190
minor
2023-02-22 16:30:57 +01:00
Jakob Rath
c76379c0cf
assign_eh: check always-false before bool-false
2023-02-22 08:58:11 +01:00
Jakob Rath
e3b3cd58ea
fix comparison of pdds with different bit-widths
2023-02-21 13:01:15 +01:00
Nikolaj Bjorner
146f0eae06
wip - arith local search
2023-02-20 12:17:14 -08:00
Nikolaj Bjorner
4aa05b2b57
remove limiting error mode #6600
2023-02-20 12:16:43 -08:00
Jakob Rath
8347c043e1
Merge remote-tracking branch 'origin/polysat' into polysat
2023-02-20 17:37:44 +01:00
Jakob Rath
33a38ba96f
simplify
2023-02-20 16:28:31 +01:00
Jakob Rath
1dea87a07a
fix add_overflow
2023-02-20 16:25:41 +01:00
Jakob Rath
455abb1db3
update
2023-02-20 16:19:56 +01:00
Jakob Rath
4cca164bb4
fix
2023-02-20 16:13:55 +01:00
Jakob Rath
d5ce9b3d5e
Try possible ule rewrite
2023-02-20 15:23:41 +01:00
Jakob Rath
b6480e789f
Repropagate may need to update watchlist
2023-02-20 15:06:31 +01:00
Jakob Rath
61ec3b9e87
log_lemma
2023-02-20 12:32:21 +01:00
Jakob Rath
1d04d08a0c
Update has_max_forbidden
2023-02-20 12:19:06 +01:00
Jakob Rath
af683ea5f9
avoid fallback to circuit
2023-02-20 12:09:11 +01:00
Jakob Rath
7f41761616
xnor
2023-02-20 11:56:23 +01:00
Jakob Rath
4501a372b1
fix boolean propagation
2023-02-20 09:39:44 +01:00
Jakob Rath
2c44018a8a
get_watch_level
2023-02-20 09:37:28 +01:00
Nikolaj Bjorner
755b517001
fix #6600
...
ensure that semantics of last-indexof(t,"") = len(t)
2023-02-19 14:02:37 -08:00
Nikolaj Bjorner
0758c93086
fix #6591
...
- 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.
2023-02-19 11:09:52 -08:00
Nikolaj Bjorner
6454e7fa3f
apply rewriting if result of destructive equality resolution is simplified
2023-02-19 11:03:04 -08:00
