Nikolaj Bjorner
0d3c29a250
handle larger buffers
2025-05-13 14:11:59 -07:00
Nikolaj Bjorner
147fb0d9c1
fix tptp5 build
2022-11-30 21:41:44 -08:00
Nikolaj Bjorner
cfc8e19baf
add more simplifiers, fix model reconstruction order for elim_unconstrained
...
- enable sat.smt in smt_tactic that
is invoked by default on first goals
add flatten-clauses
add push-ite
have tptp5 front-end pretty print SMT2 formulas a little nicer.
2022-12-01 02:35:43 +09:00
Bruce Mitchener
6835522a7f
z3++.h: No longer include unused sstream.
...
This makes some code using the C++ API have to include `<sstream>`
if they used the functionality but didn't include it themselves.
2022-08-05 09:41:49 +03:00
Nikolaj Bjorner
eacef5f3f9
deal with warnings over unused variables and procedures
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-29 19:45:35 -08:00
Nikolaj Bjorner
59e388ece1
handle bind proof constructor and print lambda
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-04 11:59:59 -07:00
Bruce Mitchener
edf8ba44d1
Switch from using Z3_bool to using bool.
...
This is a continuation of the work started by using stdbool and
continued by switching from Z3_TRUE|FALSE to true|false.
2018-11-20 11:27:09 +07:00
Florian Pigorsch
326bf401b9
Fix some spelling errors (mostly in comments).
2018-10-20 17:07:41 +02:00
Nikolaj Bjorner
ef6339f14c
fix build issues
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-01 12:00:03 -07:00
Nikolaj Bjorner
0ce2001449
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-10 11:39:22 -08:00
Nikolaj Bjorner
67c6f9be91
have the classifier revert to full arithmetic on non-difference logic, reported on http://stackoverflow.com/questions/38594208/changing-order-of-z3-fixepoint-queries-changes-the-result/38596187#3
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-26 10:32:54 -07:00
Nikolaj Bjorner
16e3a91bdf
fix issues reported by Geoff
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-21 07:56:21 -07:00
Nikolaj Bjorner
f522d995d1
apply 'to-real' coercion only on integers. bug reported by Geoff
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-20 19:03:25 -07:00
Nikolaj Bjorner
f3d657ebd1
add tptp5 example to cmake, adding output SZS directives for Geoff
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-15 12:09:23 -07:00
Nikolaj Bjorner
995e112a18
fix examples
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-20 08:01:59 -08:00
Christoph M. Wintersteiger
2818e977b6
Fixed unused variable warnings in examples.
2015-10-29 13:20:56 +00:00
Nikolaj Bjorner
d469a16bb8
add more Copyright notes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-06-10 11:59:21 -07:00
Nikolaj Bjorner
e3b1ce1fdc
also allw n-ary distrinct
...
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-05-27 10:07:09 -07:00
Nikolaj Bjorner
4f02d380aa
make use of uninterpreted_sort shorthand
...
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-05-27 09:34:47 -07:00
Nikolaj Bjorner
0e32c87dc3
fix examples and C++ API - build failure
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-15 15:43:05 +01:00
Nikolaj Bjorner
839e3fbb7c
add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-09 19:40:34 -07:00
Ken McMillan
c007a5e5bd
merged with unstable
2014-08-06 11:16:06 -07:00
Nikolaj Bjorner
861a31f458
fix build warning from tptp example
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-09-08 13:30:03 -07:00
Nikolaj Bjorner
457b22b00e
add TPTP example
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-09-06 21:49:00 -07:00
