Christoph M. Wintersteiger
|
a97358965b
|
Fixed interruption/cancelation issue in rewriter.
|
2016-11-17 16:28:49 +00:00 |
|
Nikolaj Bjorner
|
1600823435
|
fix perf bug reported in #790
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-11-17 05:38:52 +02:00 |
|
Murphy Berzish
|
fff1fadf3b
|
add str.from-int in theory_str rewriter
|
2016-11-09 15:54:22 -05:00 |
|
Christoph M. Wintersteiger
|
824ba14977
|
Disabled some ITE rewrite rules that were applied by default, but too expensive. Added re-computation of subterm occurrences in ctx_simplify_tactic. (Performance fixes for QF_LIA benchmarks).
|
2016-11-04 13:39:53 +00:00 |
|
Christoph M. Wintersteiger
|
a3e915fbea
|
Whitespace
|
2016-11-04 13:37:14 +00:00 |
|
Nikolaj Bjorner
|
be9d5c7088
|
fix evaluator for array store expressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-11-02 21:33:24 +00:00 |
|
Nikolaj Bjorner
|
ff75f88c4f
|
fix memory abuse in internalization in inc-sat-solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-31 22:25:58 +01:00 |
|
Nikolaj Bjorner
|
ca309341c3
|
fixing cancellation code paths for inc_sat_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-27 22:07:46 -07:00 |
|
Nikolaj Bjorner
|
41deae52c6
|
fix enum2bv to handle singleton enumeration types, differentiate disequality conflicts for theories that handle disequalities vs. theories that don't
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-27 13:35:53 -07:00 |
|
Nikolaj Bjorner
|
24fc19ed58
|
speed up consequence finding by avoiding local search whenver assumption level is reached during the initial phase
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-27 08:15:39 -07:00 |
|
Nikolaj Bjorner
|
da4289fadc
|
fix unit tests for pb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-25 20:47:48 -07:00 |
|
Christoph M. Wintersteiger
|
8c5c564d6c
|
fixed initialization order warning in pb2bv_rewriter
|
2016-10-25 14:31:29 +01:00 |
|
Nikolaj Bjorner
|
fefd00aa49
|
fix sign of constant in pb constraint
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-24 20:28:56 -07:00 |
|
Nikolaj Bjorner
|
b82b53dc34
|
add handling of pseudo-boolean inequalities that use if-expressions over Booleans and arihmetic instead of built-in PB predicates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-24 17:41:52 -07:00 |
|
Nikolaj Bjorner
|
6cf54a226e
|
a more efficient encoding for pseudo-Boolean inequality constraints into bit-vectors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-24 08:25:02 -07:00 |
|
Nikolaj Bjorner
|
b476784f23
|
add missing file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-23 20:52:44 -07:00 |
|
Nikolaj Bjorner
|
3778048eb4
|
add bounded-int and pb2bv solvers to fd_solver, use sorting networks for pb2bv rewriter when applicable, hoist to pb2bv_rewriter module and remove it from the pb2bv_tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-23 20:31:59 -07:00 |
|
Nikolaj Bjorner
|
23b9d3ef55
|
fix at-most-1 constraint compiler bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-22 18:50:16 -07:00 |
|
Murphy Berzish
|
ef0f6f1de3
|
add str.to-int in theory_str WIP
|
2016-10-20 16:01:51 -04:00 |
|
Nikolaj Bjorner
|
d060359f01
|
add fd solver for finite domain queries
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-18 22:34:34 -04:00 |
|
Nikolaj Bjorner
|
4fda2adec8
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-10-16 15:46:50 -04:00 |
|
Nikolaj Bjorner
|
58198d7cb6
|
add consequence finding to inc-sat-solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-16 15:45:39 -04:00 |
|
Nikolaj Bjorner
|
aec59e4ff7
|
add consequence finding to inc-sat-solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-16 15:43:28 -04:00 |
|
Christoph M. Wintersteiger
|
7e705a2d32
|
Bug fixes for underspecified FP operations.
|
2016-10-15 18:35:39 +02:00 |
|
Christoph M. Wintersteiger
|
bc257211d6
|
Whitespace
|
2016-10-15 18:35:39 +02:00 |
|
Nikolaj Bjorner
|
e3f0aff318
|
address ubuntu warning and add shortcuts for maxsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-03 16:22:13 -07:00 |
|
Nikolaj Bjorner
|
476b06fa14
|
fix compiler warnings, gcc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-09-28 16:42:07 -07:00 |
|
Mikolas Janota
|
147c0f8152
|
Removing an unused method from bv_rewriter.
|
2016-09-16 19:44:37 +01:00 |
|
Mikolas Janota
|
ec47a1df50
|
Adding bv preprocessing techniques.
|
2016-09-16 19:44:37 +01:00 |
|
Nikolaj Bjorner
|
5a86815f34
|
fix regression in seq-replace rewriting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-09-11 05:43:16 -07:00 |
|
Nikolaj Bjorner
|
0b57829bdd
|
fix heisenbug, unintialized variable, issue #720
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-09-10 11:04:29 -07:00 |
|
Nikolaj Bjorner
|
cb140011bc
|
add missing rewrite rule. Issue #731
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-09-10 09:42:36 -07:00 |
|
Nikolaj Bjorner
|
e485d1889c
|
update replace semantics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-09-08 13:59:13 -07:00 |
|
Murphy Berzish
|
f9b4f21683
|
add rewrite for theory_str rewriter RegexPlus
fixes regex-013.smt2
|
2016-08-31 19:22:04 -04:00 |
|
Murphy Berzish
|
6263391c11
|
fix out-of-range integer comparison bug in string NFA
|
2016-08-17 20:58:57 -04:00 |
|
Murphy Berzish
|
0834229b39
|
theory_str model validation for substr
|
2016-08-17 15:33:02 -04:00 |
|
Murphy Berzish
|
48081864b0
|
add regex validation in str_rewriter
|
2016-08-16 18:07:31 -04:00 |
|
Christoph M. Wintersteiger
|
e8141aaa84
|
debug fixes
|
2016-08-12 19:52:59 +01:00 |
|
Murphy Berzish
|
3dff240bb3
|
theory_str model validation for Length
|
2016-08-07 15:50:41 -04:00 |
|
Murphy Berzish
|
cb566ad5ce
|
fix model validation for theory_str
|
2016-08-07 15:43:08 -04:00 |
|
Nikolaj Bjorner
|
4958edeb42
|
fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-28 19:40:49 -07:00 |
|
Loris D'Antoni
|
73bd4acfc5
|
added symbolic automata complement for sequences
|
2016-07-28 13:50:05 -07:00 |
|
Nikolaj Bjorner
|
b7de813c63
|
set solver on simplify command
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-27 15:35:44 -07:00 |
|
Murphy Berzish
|
0f38203779
|
add RegexCharRange to theory_str
|
2016-07-19 16:39:43 -04:00 |
|
Murphy Berzish
|
9ffcd135d5
|
add RegexPlus to theory_str
|
2016-07-19 15:47:41 -04:00 |
|
Nikolaj Bjorner
|
3a70b6aab4
|
fix model generation, add rewrite rules for sin(acos(x)) reduction to help model validation. Issue #680
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-13 11:12:27 -07:00 |
|
Nikolaj Bjorner
|
d5ee7e24bc
|
add simplification for equalities between itos and constant strings, Issue #589
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-08 11:50:39 -07:00 |
|
Nikolaj Bjorner
|
30cf0d19eb
|
use of mk_bool_val
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-06-24 09:11:45 -07:00 |
|
Nikolaj Bjorner
|
f72d9c25c6
|
merge with update to bv rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-06-24 09:08:01 -07:00 |
|
Christoph M. Wintersteiger
|
70301ad3c8
|
Added bv*mul_no*flow handling in bv_rewriter.
Fixes #657.
|
2016-06-24 16:25:11 +01:00 |
|