Jakob Rath
b0e7852c9c
Upgrade bool_watch_invariant
2023-02-14 09:35:56 +01:00
Nikolaj Bjorner
3dc91de531
fix #6582
2023-02-13 13:21:30 -08:00
Nikolaj Bjorner
e07c77e072
remove redundant pre-condition
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-13 11:54:50 -08:00
Nikolaj Bjorner
4f9b277c32
more code review
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-13 11:48:19 -08:00
Nikolaj Bjorner
49b733c562
more code review
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-13 11:47:46 -08:00
Nikolaj Bjorner
bcbb39f8e5
adding cr comments in variable-elimination
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-13 10:26:51 -08:00
Nikolaj Bjorner
2b77012993
fix build
2023-02-13 08:36:12 -08:00
Nikolaj Bjorner
52804b5c8f
save on dtt
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-13 08:29:32 -08:00
Nikolaj Bjorner
7956cf1201
annotate arith_sls
2023-02-12 20:55:44 -08:00
Nikolaj Bjorner
bb81bc5452
fix #6580
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-12 20:21:53 -08:00
Nikolaj Bjorner
102eee77dc
patch regressions
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-12 20:12:01 -08:00
Nikolaj Bjorner
cac5052685
fixes related to #6577
...
- enforce elim-and in bool-rewriter when invoking hoisting.
- make cnf tactic more resilient to non-normalized input.
- enable eliminate predicates on ground formulas
2023-02-12 13:43:44 -08:00
Walden Yan
ede9e5ffc2
[WIP] More TS Binding Features ( #6412 )
...
* feat: basic quantfier support
* feat: added isQuantifier
* feat: expanded functions
* wip: (lambda broken)
* temp fix to LambdaImpl typing issue
* feat: function type inference
* formatting with prettier
* fix: imported from invalid module
* fix isBool bug and dumping to smtlib
* substitution and model.updateValue
* api to add custom func interps to model
* fix: building
* properly handling uint32 -> number conversion in z3 TS wrapper
* added simplify
* remame Add->Sum and Mul->Product
* formatting
2023-02-11 15:48:29 -08:00
Nikolaj Bjorner
5e30323b1a
wip - bounded local search for arithmetic
2023-02-11 15:46:39 -08:00
Nikolaj Bjorner
4b2c166e8b
fixes to build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-11 10:19:24 -08:00
Nikolaj Bjorner
7bef2f3e6f
wip - local search for euf/arithmetic
2023-02-11 09:33:43 -08:00
Nikolaj Bjorner
46c8d78ece
fixes for #6577
...
- the literal false should not appear in clauses
- the literal true forces a tautology
- fix early return in is_cnf check. It should check all clauses for nested Booleans.
2023-02-11 09:33:42 -08:00
Nikolaj Bjorner
d22e4aa525
wip - integrating arithmetic local search
2023-02-11 09:33:42 -08:00
Nikolaj Bjorner
1b0c76e3f0
fixes to mbqi in the new core based on #6575
2023-02-10 16:56:06 -08:00
Julian Parsert
d52e893528
Added overloaded versions of context::recfun in the c++ api that allow for the declaration of recursive functions where the domain is given by a z3::sort_vector instead of an arity and sort* ( #6576 )
...
Co-authored-by: Julian Parsert <julian.parsert@uibk.ac.at>
2023-02-10 10:00:26 -08:00
Nikolaj Bjorner
2f86d9de75
bypass assertion violation for parity
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-09 16:33:30 -08:00
Clemens Eisenhofer
6b48b25beb
Draft: Made division/remainder to op_constraints (not yet used - old code still called)
2023-02-09 23:36:15 +01:00
Jakob Rath
4813fcfe0d
re-propagate needs to be checked for all literals
2023-02-09 19:06:16 +01:00
Nikolaj Bjorner
e31eb9a6b1
add monotonicity lemma
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-09 09:31:43 -08:00
Jakob Rath
c60a2b10a5
inequality::rewrite_equiv
2023-02-09 16:33:59 +01:00
Jakob Rath
06cc15d1cc
refinement loop output
2023-02-09 16:28:52 +01:00
Nikolaj Bjorner
02d48adae5
fix #6573
2023-02-08 08:24:52 -08:00
Jakob Rath
a0f5386bdd
Use parity helper functions
2023-02-08 15:11:39 +01:00
Nikolaj Bjorner
a8335f2d5e
use phase
2023-02-07 19:50:45 -08:00
Nikolaj Bjorner
b3ebce3966
fix compilation
2023-02-07 19:30:45 -08:00
Nikolaj Bjorner
96d815b904
adding arith sls
2023-02-07 19:27:19 -08:00
Nikolaj Bjorner
6a2d60a6ba
fix #6571
...
most solvers don't support background properties
2023-02-07 11:04:58 -08:00
Nikolaj Bjorner
601e506d54
remove debug out
2023-02-07 10:40:49 -08:00
Nikolaj Bjorner
a150e58893
update release script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-07 09:21:02 -08:00
Nikolaj Bjorner
90a75866fb
elaborating on local-search rephase strategy
2023-02-07 03:17:52 -08:00
Jakob Rath
bf03886a87
elem
2023-02-07 09:57:32 +01:00
Nikolaj Bjorner
f3ae7692ca
update stage name
2023-02-06 16:08:14 -08:00
Nikolaj Bjorner
c1cadd37cc
update stage name
2023-02-06 16:07:12 -08:00
Nikolaj Bjorner
a7231027c3
try side-by-side nightly
2023-02-06 16:04:54 -08:00
Nikolaj Bjorner
c1c26f0726
restart after sat solution
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-06 09:21:35 -08:00
Jakob Rath
984e98c88f
Avoid duplicates
2023-02-06 17:52:52 +01:00
Jakob Rath
a37536e0ae
clarify unsat_core
2023-02-06 17:52:52 +01:00
Jakob Rath
c79a16db2a
Fix dependency tracking for input boolean conflicts
2023-02-06 16:28:41 +01:00
Jakob Rath
d105c1c825
Allow printing other types than unsigned
2023-02-06 16:27:38 +01:00
Jakob Rath
d7797a53df
temporary fix
2023-02-06 11:34:28 +01:00
Jakob Rath
8774952aeb
Merge remote-tracking branch 'origin/master' into polysat
2023-02-06 10:50:05 +01:00
Nikolaj Bjorner
03a4920f3d
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-05 21:41:07 -08:00
Nikolaj Bjorner
75c573877d
updates to ddfw, initial local search phase option
2023-02-05 21:35:22 -08:00
Nikolaj Bjorner
992793bd56
update nuget packaging targets #6570
2023-02-05 21:35:22 -08:00
Nikolaj Bjorner
b45f42133d
updates to try_div_monotonicity
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-04 15:55:14 -08:00
