Nikolaj Bjorner
9232ef579c
remove copy of LICENSE.txt - pypi doesn't take it
2025-05-09 16:53:45 -07:00
Nikolaj Bjorner
49dffaed39
enable pypi
2025-05-09 15:37:19 -07:00
Nikolaj Bjorner
b54ed38cea
enable pypi
2025-05-09 13:15:42 -07:00
Nikolaj Bjorner
59a7e007a4
disable pypi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-09 08:26:38 -07:00
Nikolaj Bjorner
d4b622e239
update version number
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-09 08:25:40 -07:00
Nikolaj Bjorner
a51239c641
update namespace, hoist exported functions outside of embedded namespace
2025-05-07 15:57:47 -07:00
Nikolaj Bjorner
644118660f
list euf dependency in api cmakefile
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-07 15:47:03 -07:00
Nikolaj Bjorner
eca5cd1841
mark virtual methods as override
2025-05-07 15:24:20 -07:00
Nikolaj Bjorner
9a299eb9ff
move mam to euf
2025-05-07 14:38:59 -07:00
Nikolaj Bjorner
0e4c033e30
fix #7639
2025-05-03 11:06:25 -07:00
Nikolaj Bjorner
4bedb5f8fc
fix #7638
2025-05-03 11:04:41 -07:00
Nikolaj Bjorner
dd211bade9
filter out terms that are not solved
2025-04-30 09:40:45 -07:00
Lev Nachmanson
f89e133d52
revert the behavior of add_zero_assumption ( #7631 )
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-28 16:07:46 -07:00
Nikolaj Bjorner
6af61fa0f4
remove experiment
2025-04-28 10:00:02 -07:00
Nikolaj Bjorner
b502126ebc
fix #7634
2025-04-27 23:57:57 -07:00
Nikolaj Bjorner
24090fc48c
move flush smc to first use
2025-04-27 11:44:45 -07:00
Nikolaj Bjorner
a626cd0fed
flush smc before use in model construction
2025-04-27 11:18:18 -07:00
Nikolaj Bjorner
71b5e44058
#7596 - flush smc before copy
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-04-27 10:36:27 -07:00
Nikolaj Bjorner
7a302239c2
fix #7630
2025-04-26 11:40:48 -07:00
Nikolaj Bjorner
d581dc1db4
#7630 propagate parameters on lazy tactics
2025-04-26 11:22:16 -07:00
Nuno Lopes
322e4441b3
Fix conversion of signed 1-bit BV to FP
...
Fixes https://github.com/AliveToolkit/alive2/issues/1193
2025-04-25 12:38:00 +01:00
Nikolaj Bjorner
792ffeeda7
fix latent sign bug
2025-04-23 17:22:57 -07:00
Nikolaj Bjorner
fe1fff3b7e
add scaffolding for experiments with slack
2025-04-23 17:07:50 -07:00
Nikolaj Bjorner
12ccf59ab9
rename fields to compile on c++ platforms
2025-04-23 17:06:15 -07:00
Nikolaj Bjorner
e41acd7b50
convert m_r_upper and m_r_lower bounds to plain vectors
...
manage backtracking state together with backtracking of column data.
2025-04-23 16:33:38 -07:00
Nikolaj Bjorner
fae60946bf
consolidate some bounds references
2025-04-23 15:45:44 -07:00
Nikolaj Bjorner
f6fbeda9d7
fix #7629
2025-04-23 15:22:44 -07:00
Nikolaj Bjorner
7641393f8a
use inlined functions
2025-04-23 14:28:31 -07:00
Nikolaj Bjorner
5cc57b8958
coalesce updates to bounds
2025-04-23 14:05:17 -07:00
Nikolaj Bjorner
579ba8bd70
add power axioms to arith_solver
2025-04-23 10:48:29 -07:00
Nikolaj Bjorner
d73d104ded
remove overwriting x,y,rval
2025-04-23 09:17:22 -07:00
Nikolaj Bjorner
ff920ba51b
handle root expressions, and checking exponentiation with nlsat
...
this one is for you @matthai
2025-04-22 13:47:47 -07:00
Carson Radtke
2fe2735b5e
Replace _DEBUG with Z3DEBUG ( #7628 )
...
Fixes https://github.com/Z3Prover/z3/issues/7627
2025-04-22 13:39:01 -07:00
Lev Nachmanson
a1673f2bdd
fallback to Gomory cuts and gcd conflicts if dio fails
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-21 17:10:32 -07:00
Nikolaj Bjorner
cc1bb0a255
remove superfluous makefile
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-04-19 13:56:30 -07:00
Nikolaj Bjorner
17cac7d87c
provide shortcut to command-line version to retrieve parameters
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-04-19 13:51:08 -07:00
Nikolaj Bjorner
6e88d91214
add badge for ocaml cmake
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-04-19 13:46:40 -07:00
Nikolaj Bjorner
3761dd869a
address build warning with overloaded virtual operators
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-04-19 13:42:11 -07:00
Shiwei Weng 翁士伟
f7aec02503
WIP: Migrating OCaml binding to CMake ( #7254 )
...
* Update doc for `mk_context`.
* Migrating to cmake.
* Migrating to cmake. It builds both internal or external libz3.
* Start to work on platform-specific problem.
* Messy notes.
* debug.
* Cleanup a bit.
* Fixing shared lib extension.
* Minor.
* Resume working on this PR.
* Remove including `AddOCaml`.
* Keep `z3.ml` and `z3.mli` in the src but specify the generated file in the bin.
* Keep `ml_example.ml` in the src.
* Try github action for ocaml.
* Add workflow using matrix.
* Fix mac linking once more.
* Bypass @rpath in building sanity check.
2025-04-19 13:41:27 -07:00
Lev Nachmanson
ab9f3307d6
change the default of running dio to true, and running gcd to false, remove branching in dio
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
dbde713eb3
remove testing code in is_big_term_on_no_term
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
1131d5294d
fix a bug in tracking the changes in dio
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
d289495ca4
allow gcd when dio ignores some terms
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
17af18fe31
make gcd call in dio optional
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
436eefbce2
always remove the tightened term
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
dc7185d0a4
change the name of m_changed_columns to m_changed_f_columns
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
32e77d8214
typo
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
cb1818f4b8
reject more terms with big numbers
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
1cde40bddb
dio_calls_period=4
2025-04-18 18:24:50 -07:00
Lev Nachmanson
87e2ce8948
Update lp_settings.h - m_dio_calls_period = 4
2025-04-18 18:24:50 -07:00
