Nikolaj Bjorner
3cc9d7f443
improve pre-processing
2022-04-15 12:55:26 +02:00
Nikolaj Bjorner
011c1b2dd2
remove refs to bare_str
2022-04-09 12:06:27 +02:00
Nikolaj Bjorner
f053daa051
fix #5906
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-20 11:24:42 -07:00
Nikolaj Bjorner
a9d7026724
add note about transform
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 19:13:35 -07:00
Nikolaj Bjorner
669a1d63da
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 16:36:16 -07:00
Nikolaj Bjorner
6010d751ed
fix #5903
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 16:21:47 -07:00
Hari Govind V K
f26c12a9ad
fix #5882 . Use model true when inlining ( #5892 )
2022-03-09 12:31:39 -08:00
Lorenzo Veronese
e3568d5b47
Handle additional cases in rule_properties::check_accessor ( #5821 )
...
* Handle additional cases in rule_properties::check_accessor
* Walk parents depth first in rule_properties::check_accessor
2022-03-07 07:49:59 -08:00
Nikolaj Bjorner
bbadd17d56
fix #5874
2022-03-02 08:46:28 -08:00
Nikolaj Bjorner
2b6dadcbc6
fix #5869
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-28 17:02:13 -08:00
Nikolaj Bjorner
7f149a36d7
refining model update rules for del_rule #5865 #5866
2022-02-25 08:03:46 -08:00
Nikolaj Bjorner
6be0a66b38
fix #5863
2022-02-22 13:00:20 -08:00
Nikolaj Bjorner
c2f1bdc099
fix #5862
2022-02-22 08:05:05 -08:00
Nikolaj Bjorner
d06c51d517
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-21 17:46:54 -08:00
Nikolaj Bjorner
061e94d723
#5858
...
COI model converter has to use constraints from the body and work in disjunctive mode. It needs a pre-condition that the body does not depend on other rules, in the case that it is used in a different pre-processing step for in-lining. The in-lined occurrence of the predicate has to correspond to the model construction version.
2022-02-21 17:45:00 -08:00
Nikolaj Bjorner
e8d4804dbb
Revert "use horn_subsume_model_converter in coi filter ( #5844 )" ( #5859 )
...
This reverts commit 09da87dc85
2022-02-21 04:33:52 -08:00
Nikolaj Bjorner
d0d4ab7955
#5820
2022-02-20 10:33:29 +02:00
Valentine Sobol
09da87dc85
use horn_subsume_model_converter in coi filter ( #5844 )
2022-02-16 23:35:58 +02:00
Nikolaj Bjorner
f639a7e1bc
add marker for top-level expression in rule.
2022-01-24 15:20:44 +01:00
Nikolaj Bjorner
61ab72b6a3
fix #4869
2022-01-24 15:14:47 +01:00
Nikolaj Bjorner
08294d62e5
separate dependencies for qe_lite
2022-01-12 03:26:22 -08:00
Nikolaj Bjorner
fc77345bec
breaking change. Enforce append semantics everywhere for parameter updates #5744
...
Replace semantics doesn't work with assumptions made elsewhere in code.
The remedy is to apply append (override) semantics for parameter changes.
2021-12-30 19:11:14 -08:00
Nikolaj Bjorner
6cc9aa3562
prepare user propagator declared functions for likely Clemens use case
2021-12-16 19:37:30 -08:00
Nikolaj Bjorner
a099972354
fix #5714
...
It is not unlike other fuzz bugs: it exercises some behavior that applications are unlikely to expose. In this case, a rule body expanded into a conjunction with more than 1M formulas (with a lot of repetition). The original rule representation assumed silently that the number of constraints in a body would fit within 20 bits, but reality allowed bodies with as many as 2^{32} - 1 constraints.
So "minimizing" the bug as @agurfinkel asks for seems not to make too much sense.
Just running the samples in debug mode points to the root cause.
Since fuzz bugs are not from applications and fuzz tools have the potential for creating a large number of issues, I find it reasonable to push some basic pro-active asks on filers:
- reproduce bug in debug builds to assess whether a debug assert triggers.
- minimize or keep it simpler when possible (in this case it does not apply)
- perform basic diagnostics/triage. I am basically asking to push this part of the work on to the fuzzer. Otherwise, addressing random bugs doesn't scale. Triaging should have pointed to the root cause.
Now, there tends to be something to learn from bugs. In this case, the question was: "can we avoid constraints with duplications"? In particular, it points to a basic inefficiency of extracting conjunctions (and disjunctions). The function didn't deduplicate. So I added deduplication into this function. It is used throughout z3 code base so could expose latent issues. We will see.
2021-12-16 10:20:53 -08:00
Nikolaj Bjorner
9f2b18cac5
add tactic name
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-07 13:37:57 -08:00
Henrich Lauko
96671cfc73
Add and fix a few general compiler warnings. ( #5628 )
...
* rewriter: fix unused variable warnings
* cmake: make missing non-virtual dtors error
* treewide: add missing virtual destructors
* cmake: add a few more checks
* api: add missing virtual destructor to user_propagator_base
* examples: compile cpp example with compiler warnings
* model: fix unused variable warnings
* rewriter: fix logical-op-parentheses warnings
* sat: fix unused variable warnings
* smt: fix unused variable warnings
2021-10-29 15:42:32 +02:00
Alexander Traud
1d45a33163
fix one typo and two misunderstandings for doxygen ( #5633 )
2021-10-29 15:35:05 +02:00
Alexander Traud
d1592c6abf
fix misspelled \brief for doxygen ( #5632 )
2021-10-29 15:34:28 +02:00
Nikolaj Bjorner
b723e1093b
misc warnings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-31 17:16:59 -07:00
Jakob Rath
46f8b15c14
ref/ref_vector minor convenience changes ( #5322 )
...
* Add ref_vector_core::push_back(ref<T>&&)
* Make operator bool() explicit
2021-05-31 10:27:46 -07:00
Nuno Lopes
f1e0d5dc8a
remove a hundred implicit constructors/destructors
2021-05-23 14:25:01 +01:00
Nikolaj Bjorner
4a6083836a
call it data instead of c_ptr for approaching C++11 std::vector convention.
2021-04-13 18:17:35 -07:00
Nikolaj Bjorner
15a7621e27
remove template dependency for trail objects
2021-03-19 11:15:05 -07:00
Nuno Lopes
4a3d63f9e4
NNF: dont allocate act_cache separately
2021-02-21 16:34:28 +00:00
Nuno Lopes
e773e1e78d
fix a few more warnings
2021-02-19 12:16:05 +00:00
Nuno Lopes
d6ce9cce95
fix clang warnings
2021-02-19 10:59:22 +00:00
Nuno Lopes
5e034e495f
fix compiler warnings
2021-02-19 10:33:41 +00:00
Nikolaj Bjorner
00dab30ea0
remove binary_function
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-02-18 13:18:58 -08:00
Nikolaj Bjorner
a152bb1e80
remove template Context dependency in every trail object
2021-02-08 15:41:57 -08:00
Nikolaj Bjorner
0ec567fe15
integrate v2 of lns
2021-02-04 15:47:40 -08:00
Nikolaj Bjorner
fb1509d011
expose internal API for set_phase
2021-02-02 14:29:06 -08:00
Nikolaj Bjorner
8f577d3943
remove ast_manager get_sort method entirely
2021-02-02 13:57:01 -08:00
Nikolaj Bjorner
3ae4c6e9de
refactor get_sort
2021-02-02 04:45:54 -08:00
Nikolaj Bjorner
4455f6caf8
move to get_sort as method, add opt_lns pass, disable xor simplification unless configured, fix perf bug in model converter update trail
2021-02-02 03:58:19 -08:00
Nikolaj Bjorner
22b0c3aa70
add priority queue to instantiation
2021-01-31 16:17:36 -08:00
Nikolaj Bjorner
8521d2caaa
check engine configuration for unsupported engines #4898
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-12-18 14:38:42 -08:00
Nikolaj Bjorner
f71204c222
fix #4879
2020-12-12 13:37:25 -08:00
Nikolaj Bjorner
8cb30d0505
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-12-12 12:21:34 -08:00
Nikolaj Bjorner
89fb55a864
fix #4890
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-12-12 12:20:53 -08:00
Nikolaj Bjorner
43ddb08332
fix #4874
2020-12-08 12:08:07 -08:00
