Nikolaj Bjorner
|
90400ec914
|
update C example to use new API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-16 15:03:58 -08:00 |
|
Nikolaj Bjorner
|
5ea2c22153
|
fix build break - by renaming tout to out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-06 10:21:02 -08:00 |
|
Nikolaj Bjorner
|
aeedb931f3
|
fix build break
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-06 10:20:21 -08:00 |
|
Christoph M. Wintersteiger
|
a6b3fba038
|
Build fix, hide debug code in release mode.
|
2015-11-06 18:06:23 +00:00 |
|
Christoph M. Wintersteiger
|
05e7aca388
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2015-11-06 16:24:48 +00:00 |
|
Christoph M. Wintersteiger
|
c2aee86e4e
|
Added new SMT logic names
|
2015-11-06 16:24:44 +00:00 |
|
Nikolaj Bjorner
|
deec11f24a
|
Merge pull request #296 from NikolajBjorner/master
fix for #291. The root issue is that the set of antecedents is recycl…
|
2015-11-06 07:16:44 -08:00 |
|
Nikolaj Bjorner
|
63ea2c4d8f
|
Merge pull request #295 from pazz/AstRef-hash
add __hash__ to AstRef
|
2015-11-05 16:20:10 -08:00 |
|
Nikolaj Bjorner
|
fc592fc856
|
fix for #291. The root issue is that the set of antecedents is recycled as a fixed object between routines. Antecedents that were already allocated for a Gomory cut got reset by the internalizer. This causes unsound bounds axioms to be created
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-05 15:08:42 -08:00 |
|
Patrick Totzke
|
d4242e16c5
|
add __hash__ to AstRef
AstRef objects needs to be hashable in order
to be used as keys in python dictionaries
|
2015-11-05 16:28:02 +00:00 |
|
Christoph M. Wintersteiger
|
ebbed7a92e
|
Added tactic comments for QF_AUFLIA, QF_AUFBV, QF_UF, and QF_UFBV default tactics.
|
2015-11-04 15:44:29 +00:00 |
|
Christoph M. Wintersteiger
|
7037739453
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2015-11-04 13:35:00 +00:00 |
|
Christoph M. Wintersteiger
|
715050da0b
|
Java API comments fix.
|
2015-11-04 13:34:50 +00:00 |
|
Nikolaj Bjorner
|
9ca3596f18
|
Merge pull request #289 from NikolajBjorner/master
fix rewriter for model validation
|
2015-11-03 11:17:24 -08:00 |
|
Nikolaj Bjorner
|
d6cb778365
|
fix rewriter for model validation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-03 07:45:42 -08:00 |
|
Christoph M. Wintersteiger
|
2f216ee5c1
|
Fixed PREFIX for OSX installation. Fixes #124.
|
2015-11-03 15:35:43 +00:00 |
|
Christoph M. Wintersteiger
|
bd94b59a92
|
Bugfix for arith rewriter to avoid rewriting loops.
|
2015-11-03 13:00:10 +00:00 |
|
Christoph M. Wintersteiger
|
27140c527c
|
trailing whitespace
|
2015-11-03 12:56:29 +00:00 |
|
Christoph M. Wintersteiger
|
20715bbf3b
|
Fixed initialization of interpolation context so it is properly disabled when solving SMT v1 benchmarks.
|
2015-11-03 12:29:02 +00:00 |
|
Christoph M. Wintersteiger
|
949ad4d2fc
|
Trailing whitespace removed.
|
2015-11-03 12:28:10 +00:00 |
|
Nikolaj Bjorner
|
11b6676e8f
|
Merge pull request #287 from NikolajBjorner/master
Fix bug exposed by QF_NIA example
|
2015-11-02 14:20:53 -08:00 |
|
Nikolaj Bjorner
|
2efd5bf9d1
|
Fix bug exposed in #281
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-02 14:18:49 -08:00 |
|
Nikolaj Bjorner
|
f78c769b3b
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2015-11-02 13:49:48 -08:00 |
|
Christoph M. Wintersteiger
|
7ac64f1f96
|
Bugfix for FP model converter (fp.min/fp.max models)
|
2015-11-02 19:55:25 +00:00 |
|
Nikolaj Bjorner
|
ec12368b54
|
Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-02 11:36:50 -08:00 |
|
Christoph M. Wintersteiger
|
92152b16ca
|
Bugfixes for model verification of unspecified values of fp.min/fp.max
|
2015-11-02 19:25:44 +00:00 |
|
Christoph M. Wintersteiger
|
14d2356a32
|
Code simplification
|
2015-11-02 19:25:11 +00:00 |
|
Christoph M. Wintersteiger
|
ba70ab9ad2
|
Bugfix for theory_fpa
|
2015-11-02 19:08:52 +00:00 |
|
Nikolaj Bjorner
|
77fec049a5
|
Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-02 10:27:44 -08:00 |
|
Nikolaj Bjorner
|
feba64b739
|
Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-02 10:18:25 -08:00 |
|
Nikolaj Bjorner
|
fb0999b3cf
|
Merge pull request #286 from NikolajBjorner/master
Fixes to MaxSAT, add checks for incorrect use of internalizer API
|
2015-11-02 08:25:23 -08:00 |
|
Nikolaj Bjorner
|
7169fc469e
|
Merge branch 'master' of https://github.com/NikolajBjorner/z3
|
2015-11-02 08:19:35 -08:00 |
|
Nikolaj Bjorner
|
728df41966
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2015-11-02 08:19:11 -08:00 |
|
Nikolaj Bjorner
|
653416153d
|
use appropriate MaxSAT solver even if there are no soft constraints. Also avoid PB constraints when all soft constraints are false. Reported by Klaus Becker
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-11-02 08:18:51 -08:00 |
|
Nikolaj Bjorner
|
fb624780d5
|
add checks in internalizer for issues of the form #227
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-10-31 12:41:57 -07:00 |
|
Christoph M. Wintersteiger
|
88064fc172
|
minor theory_fpa refactoring
|
2015-10-31 19:16:09 +00:00 |
|
Christoph M. Wintersteiger
|
1d7aa9ba2f
|
Fixed rewriter bug in theory_fpa.
|
2015-10-31 18:53:40 +00:00 |
|
Christoph M. Wintersteiger
|
8491b3bebe
|
Revert "Fixed use of mk_th_axiom in theory_fpa."
This reverts commit 89e99c7b4b .
|
2015-10-31 18:51:32 +00:00 |
|
Nikolaj Bjorner
|
4fd1f4a65c
|
add handler for abuse of OP_IMPLIES
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-10-31 11:34:55 -07:00 |
|
Christoph M. Wintersteiger
|
89e99c7b4b
|
Fixed use of mk_th_axiom in theory_fpa.
Relates to #227
|
2015-10-31 13:57:17 +00:00 |
|
Nikolaj Bjorner
|
2bd2dd3334
|
Merge pull request #285 from NikolajBjorner/master
add line/position information to unsupported command reports per zeph…
|
2015-10-30 21:21:13 -07:00 |
|
Nikolaj Bjorner
|
ac3edbbaaa
|
add line/position information to unsupported command reports per zeph pull request
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-10-30 19:23:31 -07:00 |
|
Nikolaj Bjorner
|
eb2193f5ae
|
Merge pull request #283 from NikolajBjorner/master
make sure to bring constraints into clausal form before using the th_…
|
2015-10-30 16:06:19 -07:00 |
|
Nikolaj Bjorner
|
b19fbe4429
|
make sure to bring constraints into clausal form before using the th_axiom assertion. Old version should not have been used as a template for copying, as in issue #227
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-10-30 15:55:18 -07:00 |
|
Nikolaj Bjorner
|
5489d60874
|
Merge pull request #282 from NikolajBjorner/master
enable further simplifications to reduce coercions
|
2015-10-30 15:13:47 -07:00 |
|
Nikolaj Bjorner
|
7838213675
|
eliminate to_real coersions to make mixed integer problems easier to digest. Issue #277
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-10-30 15:12:21 -07:00 |
|
Nikolaj Bjorner
|
997c3a234d
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2015-10-30 14:15:34 -07:00 |
|
Nikolaj Bjorner
|
b75780ce2b
|
Merge pull request #280 from NikolajBjorner/master
Add PB operators to Python API
|
2015-10-30 14:15:24 -07:00 |
|
Nikolaj Bjorner
|
f2c0a82726
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2015-10-30 14:14:23 -07:00 |
|
Christoph M. Wintersteiger
|
4923b50c53
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2015-10-30 06:31:22 -07:00 |
|