Jakob Rath
2787a22007
Backtrack/backjump based on accumulated lemmas
2022-11-23 12:49:36 +01:00
Nikolaj Bjorner
4ac5e51e3a
#6429
2022-11-23 18:35:17 +07:00
Jakob Rath
fdc186b204
Simplify constraint evaluation
2022-11-23 12:19:03 +01:00
Nikolaj Bjorner
f87e187b62
#6429
2022-11-23 17:52:14 +07:00
Nikolaj Bjorner
0a671f2f44
fix #6464
2022-11-23 17:21:51 +07:00
Nikolaj Bjorner
0a28bacd0f
remove debug out
2022-11-23 16:42:36 +07:00
Nikolaj Bjorner
9a2693bb72
tune euf-completion
2022-11-23 16:39:20 +07:00
Clemens Eisenhofer
e083f5fde8
Added missing mk_var calls
2022-11-23 10:01:20 +01:00
Nikolaj Bjorner
22353c2d6c
new core perf - add merge_tf and enable_cgc distinction
...
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
2022-11-23 11:37:24 +07:00
Nikolaj Bjorner
11b712fee0
switch to new configuration convention in solver object
2022-11-23 11:37:23 +07:00
Nikolaj Bjorner
6188c536ef
add logging of propagations to smt core
...
log theory propagations with annotation "smt".
It allows tracking theory propagations (when used in conflicts) in the clause logs similar to the new core.
2022-11-23 11:37:23 +07:00
Nikolaj Bjorner
5374142e3e
continue updates for adding proof-log to smt core
2022-11-23 11:37:23 +07:00
Nikolaj Bjorner
c7781f346d
move parameter sat.smt.proof to solver.proof.log
...
this update breaks use cases that set sat.smt.proof to True.
As it is such a new feature and the change affects possibly at most the tutorial it is made without compatibility layers.
2022-11-23 11:37:23 +07:00
Nikolaj Bjorner
cd0d52acec
using C++11 features to simplify for-loops
2022-11-23 11:37:23 +07:00
Nikolaj Bjorner
5c5673bc09
make sure parser context within solver object has its parameters updated
...
this is to enable use cases like:
```
from z3 import *
s = Solver()
OnClause(s, print)
s.set("solver.proof.check", False)
s.from_file("../satproof.smt2")
```
instead of setting global parameters before the proof replay is initialized.
2022-11-23 11:37:23 +07:00
Jakob Rath
e4999b07aa
Remove active flag from constraint
...
Superseded by boolean assignment and pwatch
2022-11-22 14:45:51 +01:00
Jakob Rath
da762700d6
quot_rem
2022-11-22 14:19:35 +01:00
Jakob Rath
85a633a3e0
Update resolve_value
2022-11-22 13:47:31 +01:00
Jakob Rath
a144a09ede
Propagation must be justified by a prefix of Gamma
2022-11-22 13:42:31 +01:00
Jakob Rath
33ea8d6e57
viable conflict also depends on vars
2022-11-22 13:40:29 +01:00
Clemens Eisenhofer
2882b92d3b
Fixed logging in Release-mode
2022-11-21 17:47:47 +01:00
Jakob Rath
6e72a97727
Refactor assignment and search state
2022-11-21 17:25:15 +01:00
Clemens Eisenhofer
b116d5ac9e
Fixed assignment bug for shifts/band
2022-11-21 16:40:28 +01:00
Clemens Eisenhofer
0341851958
Deal with special case that coefficients are multiples directly (Without calculating the symbolic inverse)
2022-11-21 14:36:01 +01:00
Clemens Eisenhofer
7cb87df00c
Bug fix; may not rewrite inequality
2022-11-21 11:34:23 +01:00
Clemens Eisenhofer
133f3d0a02
Evaluate bitwise operations on values
2022-11-21 09:38:53 +01:00
Clemens Eisenhofer
5c3180562d
Some more ways of calculating the inverse
2022-11-21 09:19:17 +01:00
Nuno Lopes
477b90228e
fix #6460 : crash in mk_to_ieee_bv_i
2022-11-20 19:19:12 +00:00
Nuno Lopes
0445d6f264
FPA->BV fix unused vars
2022-11-20 19:03:32 +00:00
Clemens Eisenhofer
5240a8382a
Make it compile again
2022-11-20 17:34:37 +01:00
Clemens Eisenhofer
4f4d56eb91
Added alternative way of calculating number of trailing zeros + hamming distance
2022-11-20 17:25:04 +01:00
Clemens Eisenhofer
98d572b48b
First try to generalize variable elimination
2022-11-20 11:35:12 +01:00
Nikolaj Bjorner
b9f34286a7
generalize macro head detection and elaboration
2022-11-20 11:36:45 +07:00
Nikolaj Bjorner
fcaa85d7a8
#6456 - elaborate on error message
2022-11-20 11:27:39 +07:00
Nikolaj Bjorner
86f3702403
prevent re-declaration of enumeration sort names
...
preventing redeclaration of all ADT cases is not part of this update.
2022-11-19 19:46:34 +07:00
Nikolaj Bjorner
c3c45f495a
add some comments to elim_predicates
2022-11-19 19:45:25 +07:00
Nikolaj Bjorner
251d49d133
remove outdated comment
2022-11-19 18:55:30 +07:00
Nikolaj Bjorner
3f10933225
remove VERBOSE 0
2022-11-19 18:55:01 +07:00
Nikolaj Bjorner
771157696b
new simplifier/tactic
...
eliminate_predicates finds macros and eliminates predicates from formulas as pre-processing.
2022-11-19 18:51:20 +07:00
Nikolaj Bjorner
d735faae4e
add isolated hide/add model converter functions
2022-11-19 18:50:37 +07:00
Nikolaj Bjorner
a81a5ec68c
add virtual function requirement to dependent_expr_state
2022-11-19 18:46:31 +07:00
Nikolaj Bjorner
dcc995f0e5
code simplification
2022-11-19 18:45:54 +07:00
Nikolaj Bjorner
41b40c3a51
remove dead code
2022-11-19 18:45:07 +07:00
Nikolaj Bjorner
c2e9016d04
display model-add parameters in correct order
2022-11-19 18:44:52 +07:00
Nikolaj Bjorner
ba68652c72
add destructive equality resolution to existentials
2022-11-19 18:43:46 +07:00
Nikolaj Bjorner
7da91f4313
allow printing declarations with reverse variable order
2022-11-19 18:43:21 +07:00
Jakob Rath
022c06f75d
pdd::subst_get
2022-11-18 15:14:38 +01:00
Jakob Rath
adc9f7abe4
Add basic implementation of left shift
2022-11-17 17:37:52 +01:00
Jakob Rath
68707eefe7
Fix lshr axioms
2022-11-17 17:37:52 +01:00
Jakob Rath
80a2ac64de
Remove tst_polysat_argv
2022-11-17 17:37:52 +01:00
