Josh Berdine
8d81a2dcaf
Note that Z3_get_numeral_small is essentially redundant ( #7599 )
...
* Check that Z3_get_numeral_small is given non-null out params
Analogous to other Z3_get_numeral_* functions with out params.
* Note that Z3_get_numeral_small is essentially redundant
The error behavior of Z3_get_numeral_small does not follow the pattern of
the other functions. The functions that have out params and return a bool
indicating success (such as Z3_get_numeral_rational_int64) return false
rather than signaling an error when given an unsupported expression
argument (such as a rounding mode value). The functions that do not have out
params signal an error in such cases. Z3_get_numeral_small is the odd one
out in that it signals errors and returns a status bool.
This error handling is the only difference between Z3_get_numeral_small and
Z3_get_numeral_rational_int64, so this patch adds a comment to the
documentation.
2025-03-29 10:02:32 -07:00
Josh Berdine
63ad2837e2
Add Z3_get_array_arity ( #7598 )
2025-03-28 14:42:51 -07:00
Josh Berdine
934455a24b
Remove vestiges of old ml api ( #7597 )
2025-03-27 16:41:31 -07:00
Lev Nachmanson
e4897fff00
replace Exists by ForAll in the mathematica lemmas
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-27 12:32:37 -07:00
Lev Nachmanson
39df8999c8
enable shorterter mathematica printouts in nlsat
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-27 12:23:32 -07:00
Nikolaj Bjorner
e86a918ae7
turn on ite simplification by default
2025-03-26 11:30:08 -07:00
Nikolaj Bjorner
8368094618
fix indentation
2025-03-25 21:27:38 -07:00
Nikolaj Bjorner
4fd6ba442a
replace costly ite reduction by disjointnes check
2025-03-25 21:15:03 -07:00
Nikolaj Bjorner
392bc166a3
optimize bool rewriter
2025-03-25 14:07:52 -07:00
Nikolaj Bjorner
29712503a0
add option to rewrite ite value trees
2025-03-25 11:09:56 -07:00
Lev Nachmanson
e92ccddb23
change line breaks
2025-03-24 15:38:57 -10:00
Lev Nachmanson
17bd02d1a3
change a comment
2025-03-24 15:29:19 -10:00
Nikolaj Bjorner
8bbe752d7d
remove dead code
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 12:47:23 -07:00
Nikolaj Bjorner
7e4a1f246e
fix crash in elim_constr2
2025-03-24 12:36:13 -07:00
Nikolaj Bjorner
93cf989b78
household chores - move to iterators
2025-03-24 12:36:13 -07:00
Lev Nachmanson
dee3cf8de4
remove an unused field
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
9302a02a81
reintroduce m_var_register, and avoid modulo gcd in normalize conflicts
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
9a62ed5ab2
added some comments
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
c634701b8f
formatting
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
f073da9edd
cleaning up the inner tightening code
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
8c96178c0b
avoid the variable mapping to m_ematrix and suppressing redundand constraints
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
29c5c20267
use more descriptive functions than casting comparisons
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
7fb40e86eb
tidy
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
a41bd38a3a
use pattern of matching with undef instead of matching with conflict to reduce assumptions on procedure contracts
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
676a536e9e
fix a print out
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
d507d0fdb4
attempt to use the gcd of fixed vars
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
f181e3aa81
add comment on derivation of bound
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
dd19b381d8
detect more m_terms_to_tighten
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
307af0fd97
remove an unused field
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
fc1c8c4cc4
add public access to bijection key_val iterator
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
8b5510bcd6
nit
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
7577f6fea0
neatify loops
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
f091b6ffdd
remove 'unsat' move, we already have 'conflict'. Add display for cancelled
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
1af2474f7b
code review updates, tidy pretty printer for column info
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
32028083fb
fix bug introduced while absstracting m_conflict_index
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
f3b34fd835
isolate m_conflict_index functionality
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
ff5ae4d1ed
add systematic way to combine lia_move results
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
00277ba3cf
nits
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
488c74d3cc
print also column values
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
22cfab3d42
remove term sorting by the span
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
12203fc69a
sort terms by weight for tightening
2025-03-24 07:44:13 -10:00
Lev Nachmanson
0a3c118701
more aggressive term tightening
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
50418fa170
try another sorting of terms to tighten
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
ec7c61569d
separate m_changed_terms and m_terms_to_tighten in indexed_uint_sets
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
7c12a029e2
detect non integral terms in dio
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
a62d664ae4
testing! disable gomory cut in int_solver
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
5e2d000369
optimize entrry recalculation
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
ecfbdbbd23
allow bounds tightening on fixed columns
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
f501aea3eb
add comments and renaming
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00
Lev Nachmanson
a522e81652
profile and remove dead code from dioph_eq.cpp
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-03-24 07:44:13 -10:00