Nikolaj Bjorner
5d17e28667
support for smtlib2.6 datatype parsing
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-09-04 21:12:43 -07:00
Nikolaj Bjorner
a3dba5b2f9
hide new datatype plugin
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-09-03 20:01:59 -07:00
Nikolaj Bjorner
a887475e9f
remove dom-simplifier from build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-09-03 15:01:54 -07:00
Nikolaj Bjorner
009e94d188
update to theory_seq following examples from PJLJ
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-30 14:00:01 -07:00
Nikolaj Bjorner
4452ff9884
elaborate on dom simplifier
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-29 19:16:56 -07:00
Nikolaj Bjorner
6969e6024b
merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-29 17:42:48 -07:00
Nikolaj Bjorner
8d8e4cbc51
fix some basic mistakes in dominator code
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-28 20:11:46 -07:00
Nikolaj Bjorner
597f77cd77
initial sketch for dominator based simplifiation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-28 20:03:31 -07:00
Nikolaj Bjorner
5db349f6fa
raise an exception if trying proof generation for the SAT solver. Stackoverflow question https://stackoverflow.com/questions/45885321/check-function-while-qf-fd-logic-is-set-throws-accessviolationexception
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-27 23:52:27 -07:00
Nikolaj Bjorner
3bfc3437f1
purify
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-27 11:57:13 -07:00
Nikolaj Bjorner
d940516df3
fixes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-27 11:01:45 -07:00
Nikolaj Bjorner
2ede4b2c80
fixes based on regression tests
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-27 09:31:16 -07:00
Nikolaj Bjorner
2955b0c2ef
removing more dependencies
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-26 03:05:34 -07:00
Nikolaj Bjorner
c03be16039
merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-26 01:33:19 -07:00
Christoph M. Wintersteiger
b8a81bcb09
Added unsat core support to the macro-finder.
2017-08-25 20:21:57 +01:00
Christoph M. Wintersteiger
227e6801c2
Whitespace
2017-08-24 18:33:21 +01:00
Nikolaj Bjorner
8ff8470809
Merge branch 'master' of https://github.com/z3prover/z3
2017-08-23 16:33:54 -07:00
Nikolaj Bjorner
f062e17037
remove simplifier dependencies from ufbv tactics
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-23 12:30:33 -07:00
Nicolas Braud-Santoni
b877c962ca
injectivity: Add tactic to CMake-based builds
2017-08-23 10:27:55 +00:00
Nicolas Braud-Santoni
ae9ace2321
injectivity: Cleanup whitespace
2017-08-23 10:25:33 +00:00
Nikolaj Bjorner
ce04c18a7a
trying to get rid of last simplifier dependency in macros
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-22 22:14:13 -07:00
Nikolaj Bjorner
e2b46257d6
reducing dependencies on simplifier
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-22 15:09:34 -07:00
Nicolas Braud-Santoni
27fd879b8c
injectivity: Fixup rewriter
2017-08-22 18:44:34 +00:00
Nicolas Braud-Santoni
33dd168195
Remove unnecessary parameter
2017-08-22 18:09:57 +00:00
Nicolas Braud-Santoni
c0b6d00e8a
Update debug output
2017-08-22 18:09:38 +00:00
Nicolas Braud-Santoni
4cb7f72509
First version of the inj. tactic
2017-08-22 17:10:20 +00:00
Nikolaj Bjorner
97e263299d
add logic 'SAT' as an alternative name to QF_FD some solverFor(SAT) works too. #1152
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-15 01:35:28 -07:00
Nuno Lopes
000796c25c
micro-optimization in tactics' cleanup(): avoid dealloc+alloc traffic
2017-08-14 20:12:00 +01:00
Nikolaj Bjorner
f99048f3e7
rewrite to address some cases like #1203 , updates to division handling in NRA
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-12 13:24:54 -07:00
Nikolaj Bjorner
2b82fd5d0c
updated include directives
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-01 10:51:47 -07:00
Nikolaj Bjorner
b19f94ae5b
make include paths uniformly use path relative to src. #534
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 13:24:11 -07:00
Christoph M. Wintersteiger
943dc8118a
Improved collect-statistics tactic
2017-07-20 13:44:47 +01:00
Nikolaj Bjorner
49cf3f8008
update documentation according to #1058
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-07 07:44:55 -07:00
Nikolaj Bjorner
d66db280a8
fix compiler warnings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-04 13:43:32 -07:00
Nikolaj Bjorner
08524a2d90
cleanup for warning message
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-01 11:47:17 -07:00
Nikolaj Bjorner
1fee5fd94e
Merge pull request #1094 from delcypher/cmake_fix_generated_cpp_deps
...
[WIP][CMake] Fix broken regeneration of some .cpp files
2017-06-21 17:47:41 -07:00
Dan Liew
229fd3dc3e
[CMake] Fix dependencies for generating install_tactic.cpp
.
...
Previously CMake was not aware of which headers files the generation
of `install_tactic.cpp` depended on. Consequently this could result
in broken incremental builds if
* Existing headers that declared tactics/probes changed.
* New tactics/probes were added to new header files.
Now the `z3_add_component()` CMake function has been modifed to take an
optional `TACTIC_HEADERS` argument which allows the headers that declare
tactics/probes to be explicitly listed. The necessary component
declarations have been modified to declare their tactic/probe header
files.
With this information CMake will now regenerate `install_tactic.cpp`
correctly.
This required the `mk_install_tactic_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.
This partially fixes #1030 .
2017-06-21 23:03:48 +01:00
Nikolaj Bjorner
b516f22549
refine test for non-fd to be more inclusive while addressing #1092
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-21 08:01:03 -07:00
Nikolaj Bjorner
a3ee785923
disable dt2bv for quantified variables as enum2bv does not handle them. #1092
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-21 07:29:21 -07:00
Arie Gurfinkel
625874e66f
remove debug code
2017-06-20 21:07:38 -04:00
Nikolaj Bjorner
d3320f8b81
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-14 21:48:19 -07:00
Nikolaj Bjorner
8ac43c981a
use less memory #1078
2017-06-14 21:41:24 -07:00
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