Nikolaj Bjorner
|
e9e0293d1a
|
local updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-02-02 10:19:51 -08:00 |
|
Nikolaj Bjorner
|
7faa35ebdb
|
fixing card
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-31 18:47:30 -08:00 |
|
Nikolaj Bjorner
|
8b7bafbd9f
|
updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-30 21:23:53 -08:00 |
|
Nikolaj Bjorner
|
13099b1590
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-19 17:56:43 -08:00 |
|
Nikolaj Bjorner
|
24eae3f6e0
|
fix crash with unary xor #870
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-15 12:06:56 -08:00 |
|
Nikolaj Bjorner
|
cb6c6332b3
|
update conflict resolution for cardinality case
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-12-28 12:44:30 -08:00 |
|
Nikolaj Bjorner
|
4bcf1bf2f6
|
fix debug build, unused variable warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-12-21 10:44:49 -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
|
c1480b4389
|
handle model generation from issue #748. Deal with warnings from #836
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-12-12 00:40:52 +01:00 |
|
Nikolaj Bjorner
|
7cc093eee0
|
Add rewrite rule for property encoded in #812
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-12-11 11:05:12 +01:00 |
|
Nikolaj Bjorner
|
32c63ce4cd
|
address other warnings per input from delcypher
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-12-10 17:23:59 +01:00 |
|
Nikolaj Bjorner
|
8e6600c6be
|
add python API for newly exposed regex constructors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-12-09 09:09:03 +01:00 |
|
Nuno Lopes
|
e697d3e810
|
remove 2 outdated comments
|
2016-12-01 14:10:31 +00:00 |
|
Nikolaj Bjorner
|
7a4c20698f
|
fix handling of AC operator ++ on regular expressions. Issue #804
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-11-22 13:02:17 -08:00 |
|
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 |
|
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 |
|
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 |
|
Christoph M. Wintersteiger
|
e8141aaa84
|
debug fixes
|
2016-08-12 19:52:59 +01: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 |
|