Dan Liew
4b517b96df
[CMake] Move CMake files into their intended location so the
...
`contrib/cmake/bootstrap.py` script no longer needs to be executed.
The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461 . While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.
The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.
This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
2017-06-12 11:59:00 +01:00
Christoph M. Wintersteiger
a7d5bb7b36
Tabs
2017-05-31 12:18:00 +01:00
Nikolaj Bjorner
29a49f4427
convert static random fields to non-static
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 16:46:07 -07:00
Nikolaj Bjorner
9b3e2a9afe
re-enable LRA after fixing dispatch for LRA in smt-setup
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 09:16:07 -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
67513a2cf5
fix detection of bounds under conjunctions. Issue #971
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-04-11 07:40:09 +08:00
Christoph M. Wintersteiger
27a1758857
Added rewriter.ignore_patterns_on_ground_qbody option to disable simplification of quantifiers that have their universals appear only in patterns, but otherwise have a ground body.
2017-04-07 21:19:20 +01:00
Nikolaj Bjorner
29969648ba
check that formulas are in lira before invoking qsat. Issue #919
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-03-09 05:52:46 +01:00
Nikolaj Bjorner
fcda4cee9f
ensure evaluation of array equalities is enabled for external facing evaluator. Issue #917
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-03-09 05:29:56 +01:00
Nikolaj Bjorner
899843b7cd
fix unhandled finite domain sort rewrite case. Issue #918
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-02-26 17:20:54 -08:00
Nikolaj Bjorner
e02160c674
expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-02-24 11:07:40 -08:00
Christoph M. Wintersteiger
e4411265ea
Fixed model-converter segfault in ::check_sat. Relates to #881
2017-02-05 17:53:44 +00:00
Christoph M. Wintersteiger
54280b6cc5
Fixed model-converter segfault in ::check_sat. Relates to #881
2017-02-05 17:20:45 +00:00
Christoph M. Wintersteiger
d6b4e99489
Fixed signed/unsigned warnings
2017-02-05 16:03:00 +00:00
Christoph M. Wintersteiger
5682c43604
Merge pull request #881 from dwoos/tactic-labels
...
Thread labels through tactic system
2017-02-04 20:37:11 +00:00
Christoph M. Wintersteiger
c56edc63d2
Merge pull request #882 from dwoos/sine-filter
...
Add basic Sine Qua Non filtering
2017-02-04 20:24:09 +00:00
Doug Woos
d6fbfe401e
add and use new is_pattern recognizer
2017-02-01 16:21:15 -08:00
Doug Woos
44c417904b
correctly pretty-print
2017-02-01 16:21:01 -08:00
Doug Woos
a147e2bc35
use is_uninterp
2017-02-01 16:20:40 -08:00
Nikolaj Bjorner
40177f7bac
bypass combined solver when logic is set to QF_FD
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-02-01 08:05:04 -08:00
Nikolaj Bjorner
4d8d705b3f
bypass combined solver when logic is set to QF_BV or QF_FD
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-02-01 08:02:24 -08:00
Doug Woos
d9e43f0e6d
use insert_if_not_there
2017-01-31 11:48:52 -08:00
Doug Woos
89ba99918e
reindent
2017-01-31 11:48:52 -08:00
Doug Woos
c0bb6dd2be
delete unused args
2017-01-31 11:48:51 -08:00
Doug Woos
da63f6b0ff
delete comment
2017-01-31 11:48:51 -08:00
Doug Woos
b00c4d2e64
add name
2017-01-31 11:48:51 -08:00
Doug Woos
8196173e29
Introduce and use labels_vec
2017-01-30 15:50:34 -08:00
Doug Woos
3791810920
add const &
2017-01-30 15:09:57 -08:00
Nikolaj Bjorner
37ee4c95c3
adding parallel threads
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-01-30 02:09:08 -08:00
Doug Woos
a9d61d48ae
Add basic Sine Qua Non filtering
2017-01-27 11:22:39 -08:00
Doug Woos
5796e15088
Thread labels through tactic system
2017-01-27 11:07:13 -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
20790c46ee
bail out on failure to properly project
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-12-11 04:23:07 +01:00
Nikolaj Bjorner
fe10f2d244
address #835
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-12-10 07:51:16 +01:00
Nikolaj Bjorner
e092232f67
add virtual destructors, fix operator code for API methods complement and intersection per note by Loris d'Antoni
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-12-09 23:17:52 +01:00
Nuno Lopes
dedae29300
add a few more statics to avoid symbol clashes
2016-12-01 17:37:07 +00:00
Nuno Lopes
42b26c63e5
make a few functions static
2016-12-01 14:01:20 +00:00
Christoph M. Wintersteiger
b1f7c6ac97
eliminated unnecessary variable
2016-11-04 22:08:49 +00: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
f61600d1d8
fixing unsat core extraction for tactics
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-11-02 14:14:55 +00:00
Nikolaj Bjorner
305e080239
enable unsat core extraction in nlsat_tactic
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-11-01 17:57:28 +01: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
2475f3bff5
ensure that variables passed to consequence finding have bound constraints, if applicable. Even if those variables do not occur in the constraints
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-10-28 07:41:27 -07:00
Christoph M. Wintersteiger
f1412d3f32
Bugfix for bouned_int2bv_solver
2016-10-28 14:23:01 +01:00
Christoph M. Wintersteiger
02e1bae9cb
whitespace
2016-10-28 14:22:27 +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
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
461e88e34c
additional robustness check for incremental sat solver core when it recieves interpreted constants, added PB equality to interface and special handling of equalities to adddress performance gap documented in #755
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-10-25 20:32:13 -07:00
