mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
6872 commits 24 branches 48 tags 158 MiB
Commit graph

236 commits

Author SHA1 Message Date
Nikolaj Bjorner
8acb37e734 revert change to 1065 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-10 09:45:18 -07:00
Nikolaj Bjorner
b8e8e090ad filter assumptions by membership in initial list #1065 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-10 09:30:01 -07:00
Nikolaj Bjorner
efd5727676 add shorthand for enumerating constants in a model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-02 10:35:09 -07:00
Nikolaj Bjorner
49faaaa8f1 allowing non-literal assumptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 15:01:00 -07:00
Nikolaj Bjorner
21cda27f5e fix quadratic behavior of extract_assumptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 15:57:31 -07:00
Nikolaj Bjorner
ed0b2be618 fix bug in tracking levels of variables: levels are not cleared, only truth assignment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 14:10:07 -07:00
Nikolaj Bjorner
f9105edb14 revert to native chunker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 15:22:52 -07:00
Nikolaj Bjorner
d14f2af5ae deal with subtraction that manages to sneak in. Issue #996 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 15:22:06 -07:00
Nikolaj Bjorner
d6e2e1f28f Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-30 11:28:26 -07:00
Nikolaj Bjorner
aff02ca905 include 'stopwatch.h' to avoid ODR warnings, #994 2017-04-30 11:28:11 -07:00
Nikolaj Bjorner
5fcbf55216 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-30 10:23:05 -07:00
Nikolaj Bjorner
2c208e1d10 Sat update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 10:23:00 -07:00
Nikolaj Bjorner
fa868e058e fix bound bug #991 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 17:39:02 -07:00
Nikolaj Bjorner
8032217fd1 tuning and fixing consequence finding, adding dimacs evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-26 13:53:37 -07:00
Nikolaj Bjorner
dedc130e98 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-25 10:30:16 -07:00
Nikolaj Bjorner
34acaa8f56 update license for space/quotes per #982 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-24 13:34:10 -07:00
Nikolaj Bjorner
ec29a03c8f add facility to dispense with cancellation (not activated at this point). Address #961 by expanding recurisve function definitions that are not tautologies if the current model does not validate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-07 21:22:38 -07:00
Nikolaj Bjorner
723b507a88 properly handle recursive function definitions #898 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-24 10:11:39 -07:00
Nikolaj Bjorner
e05cee757b properly handle recursive function definitions #898 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-24 10:10:42 -07:00
Christoph M. Wintersteiger
0399e5e2d3 Fixed variable initialization warning 2017-03-24 14:49:24 +00:00
Nikolaj Bjorner
26ae3a5abb making simplifier code exception friendlier. Towards getting a handle on #939 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-22 19:06:59 -07:00
Nikolaj Bjorner
e47e8c67c0 introducing scoped detacth/attach of clauses to enforce basic sat solver invariants. Part of investigating #939: 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-22 14:12:47 -07:00
Nikolaj Bjorner
72651e2e98 fixing sources for double frees of clauses. #940 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-14 19:35:11 -07:00
Nikolaj Bjorner
bd0bd6052a Merge branch 'master' of https://github.com/Z3Prover/z3 2017-02-02 10:19:21 -08:00
Nikolaj Bjorner
9ca52a3361 fix bug in lexicographic handling in maxres: previous assumptions were not committed in corner cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-02 10:19:11 -08:00
Nikolaj Bjorner
9cfd412cd0 enable pb theory always as pb terms can be introduced during transformations. Issue #884 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-01 15:28:29 -08:00
Nikolaj Bjorner
256a0e2d82 move exchange par 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-01 12:12:26 -08:00
Nikolaj Bjorner
f015e3e4cc fix bug in propagation of parameters to combined solvers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-31 17:17:58 -08:00
Nikolaj Bjorner
bdfa84c6fe fix issues with running parallel solver: random strategy should not be a default on all solvers. Also reuse base solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-31 13:22:03 -08:00
Nikolaj Bjorner
1d1949e395 ensure that parallel threads are only invoked when thread count > 1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 18:30:06 -08:00
Nikolaj Bjorner
76bc4f0b38 refine parsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 11:30:42 -08:00
Nikolaj Bjorner
37ee4c95c3 adding parallel threads 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 02:09:08 -08:00
Nikolaj Bjorner
962979b09c rework sat.mus to use restart count for bounded minimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-26 13:28:40 -08:00
Nikolaj Bjorner
4782e19086 fix bug in sat-simplifier decreasing heap values of variables that are not in the heap 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 16:21:51 -08:00
Nikolaj Bjorner
873d975c77 fix bug in consequence extraction: the order of bcp is not fixed between restarts, so the order of unit literals may not be preserved. This is relatively rare, so we optimize for the case where we assume bcp preserves order (and maybe miss some consequences) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-17 13:41:15 -08:00
Nikolaj Bjorner
7df803c131 Fix unsound handling of upper bounds in wmax, thanks to Patrick Trentin for report and careful repros #847 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 11:52:48 -08:00
Nikolaj Bjorner
bc6b3007de remove unused features related to weighted check-sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-13 20:53:22 -08:00
Nikolaj Bjorner
c69a86e647 fix bug in antecedent collection for consequence finding: once an antecedent is set, it should not be cleared 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-06 19:34:50 -05:00
Christoph M. Wintersteiger
cb75a55095 Fixed initialization order warning. 2017-01-03 13:41:08 +00:00
Nikolaj Bjorner
74d3de01b3 enable incremental consequence finding with restart timeout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-02 10:07:02 -08:00
Nikolaj Bjorner
a4d5c4a00a make get_consequence call skip check-sat if a model is already there 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-30 18:05:19 -08:00
Nikolaj Bjorner
aaf6e67ec8 add restart.max parameter to control cancellation based on restart count 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-25 17:43:47 -08:00
Nikolaj Bjorner
df492e200f merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:04:02 -08:00
Nikolaj Bjorner
8d18fd075e remove sources for unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 09:54:45 -08:00
Nikolaj Bjorner
189d449cff fix generation of wcnf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-18 14:49:45 -08:00
Nikolaj Bjorner
d9227b95ea blast distinct in incremental BV solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-29 15:45:23 -08:00
Christoph M. Wintersteiger
1799310155 Fixed iterator invalidation bug in SAT probing. Relates to #798. 2016-11-26 14:07:05 +00:00
Nikolaj Bjorner
ea601dd403 fix and coallesce clique functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-19 03:55:48 -08:00
Christoph M. Wintersteiger
bfaa9ddf63 Fixed potential SAT solver cleanup problem. Renamed functions for consistency. Relates to #570. 2016-11-14 17:42:21 +00:00
Christoph M. Wintersteiger
520e868add Fixed interruption cleanup bug in sat_solver. Relates to #570. 2016-11-14 17:42:20 +00:00