Nikolaj Bjorner
ff68df3451
update output of z3 doc
2022-11-08 16:10:50 -08:00
Nikolaj Bjorner
254f7b97ef
cleanup state to clear model trail during calls.
2022-11-08 15:56:10 -08:00
Nikolaj Bjorner
823cd23ecc
building x64 windows tests during ci is too slow, skipping tests
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-08 15:37:56 -08:00
Nikolaj Bjorner
3faca52c40
re-enable new solve_eqs with bug fixes
2022-11-08 14:17:17 -08:00
Nikolaj Bjorner
9ef78fcfa7
revert new solve-eqs
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-08 13:57:58 -08:00
Nikolaj Bjorner
3a37cfca30
switch to solve_eqs2 tactic
2022-11-08 12:23:36 -08:00
Nikolaj Bjorner
f769e2f1f6
have bool rewriter use flat_and_or, and integrate hoist rewriter
2022-11-08 12:21:50 -08:00
Nikolaj Bjorner
238ea0a264
add shorthands for concatentation
2022-11-08 12:21:25 -08:00
Nikolaj Bjorner
3a4b8e2334
add rewrite rules to bv-rewriter
2022-11-08 12:20:51 -08:00
Nikolaj Bjorner
a34701471f
clean up hoist rewriter
2022-11-08 12:20:25 -08:00
Nikolaj Bjorner
ab36f86843
add handler for reporting statistics
2022-11-08 12:19:48 -08:00
Nikolaj Bjorner
8afec86fe8
add option for flat_and_or
2022-11-08 12:19:27 -08:00
Nikolaj Bjorner
10fb71cf93
better error description for configuring restart
2022-11-08 12:18:45 -08:00
Nikolaj Bjorner
cbc5b1f4f6
have theory_recfun use recursive function discriminator to control when it is enabled
2022-11-06 12:09:45 -08:00
Nikolaj Bjorner
f004478565
produce tseitin justification for clause proofs when a clause is a "gate".
2022-11-06 12:00:25 -08:00
Nikolaj Bjorner
53b6059276
bypass built-in proof objects for clause trail
...
the build-in proof constructors are not flexible when it comes to allowing alternation of justified lemmas and lemmas without justifications.
2022-11-06 11:59:56 -08:00
Nikolaj Bjorner
8ff1e44a95
add discriminator to whether context contains recursive functions to avoid enabling recursive function solver when there are just macros
2022-11-06 11:58:21 -08:00
Nikolaj Bjorner
a4c2a2b22c
use ast_util::mk_not to avoid redundant double negations during nff
2022-11-06 11:57:46 -08:00
Nikolaj Bjorner
78f9e6b31a
extend error type message with more information - display the arguments that are passed
2022-11-06 11:57:21 -08:00
Nikolaj Bjorner
4c1a3fab64
fix #6442
2022-11-05 23:15:03 -07:00
Nikolaj Bjorner
d8133a47c2
Update solve_eqs.cpp
2022-11-05 22:47:46 -07:00
Nikolaj Bjorner
6c12aaad74
wip - testing solve-eqs2, added as tactic
2022-11-05 22:42:59 -07:00
Nikolaj Bjorner
4d8860c0bc
wip - adding context equation solver
...
the solve_eqs_tactic is to be replaced by a re-implementation that uses solve_eqs in the simplifiers directory.
The re-implementation should address efficiency issues with the previous code.
At this point it punts on low level proofs. The plan is to use coarser
dependency tracking instead of low level proofs for pre-processing. Dependencies can be converted into a proof hint representation that can be checked using a stronger checker.
2022-11-05 10:34:57 -07:00
Nikolaj Bjorner
ae2672f132
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-04 14:11:24 -07:00
Nikolaj Bjorner
154b09309b
fixing build, wip on model reconstruction integration into dependent-expr-state
2022-11-04 14:04:44 -07:00
Nikolaj Bjorner
7bb962d934
add ad-hoc any-of for cross compatibility and simplifying interface
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-04 12:49:55 -07:00
Nikolaj Bjorner
49d1490454
add ad-hoc any-of for cross compatibility and simplifying interface
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-04 12:48:30 -07:00
Nikolaj Bjorner
de9368bab0
Update expr_replacer.h
2022-11-04 11:25:39 -07:00
Nikolaj Bjorner
28668c6efc
set up model reconstruction trail
2022-11-04 11:25:39 -07:00
Nikolaj Bjorner
84af521514
fixes #6439 #6436
2022-11-04 09:36:06 -07:00
Nikolaj Bjorner
626380b3c7
fixing build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-03 22:08:21 -07:00
Nikolaj Bjorner
e8112a6564
add initial stubs for model reconstruction trail
2022-11-03 21:35:07 -07:00
Nikolaj Bjorner
9007bdf780
move horn_subsume_model_converter to ast/converters
2022-11-03 20:26:02 -07:00
Nikolaj Bjorner
25bb935793
move more converters
2022-11-03 20:18:21 -07:00
Nikolaj Bjorner
06eb460c75
move tactic_params to params
2022-11-03 05:50:46 -07:00
Nikolaj Bjorner
203652da74
add converters module to python build
2022-11-03 05:26:06 -07:00
Nikolaj Bjorner
ba6b21d7d4
Create solve_eqs2_tactic.h
2022-11-03 05:23:38 -07:00
Nikolaj Bjorner
1dca6402fb
move model and proof converters to self-contained module
2022-11-03 05:23:01 -07:00
Nikolaj Bjorner
7b12a5c5a8
build fix
2022-11-03 04:49:20 -07:00
Nikolaj Bjorner
90490cb22f
make visited_helper independent of literals
...
re-introduce shorthands in sat::solver for visited and have them convert literals to unsigned.
2022-11-03 03:54:39 -07:00
Nikolaj Bjorner
070c5c624a
wip - converting the equation solver as a simplifier
2022-11-03 03:35:30 -07:00
Nikolaj Bjorner
6841ba3e57
Update .gitignore
2022-11-03 03:35:30 -07:00
Nikolaj Bjorner
c0f483528d
working on solve_eqs
2022-11-03 03:35:29 -07:00
Nikolaj Bjorner
e141759768
init solve_eqs
2022-11-03 03:35:29 -07:00
Clemens Eisenhofer
6790f18132
Added limit to "visit" to allow detecting multiple visits ( #6435 )
...
* 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
* Added limit to "visit" to allow detecting multiple visits
* Putting visit in a separate class
(Reason: We will probably need two of them in the sat::solver)
* Bugfix
2022-11-03 03:34:52 -07:00
Nikolaj Bjorner
e0bbe8dfc0
Merge branch 'master' of https://github.com/z3prover/z3
2022-11-02 17:32:32 -07:00
Nikolaj Bjorner
df71e83428
remove incorrect assertion
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-02 17:32:09 -07:00
Clemens Eisenhofer
ae707ffff7
Added 64-bit "1" counting ( #6434 )
...
* 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
* Added 64-bit "1" counting
2022-11-02 10:02:29 -07:00
Nikolaj Bjorner
0d97d2214c
adding virtual destructor
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-02 09:37:55 -07:00
Nikolaj Bjorner
41b87b4c42
Create bv_slice_tactic.cpp
...
missing file
2022-11-02 08:51:43 -07:00
