Nikolaj Bjorner
811cd9d48d
add example
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-03 09:14:47 -08:00
Nikolaj Bjorner
ee18c5070c
add stubs for injective function axioms, add some parameter functions
2022-03-03 09:09:03 -08:00
Nikolaj Bjorner
757cf7622d
sketch ArrayValue, add statistics
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-02 10:59:19 -08:00
Nikolaj Bjorner
80506dfdfa
sketch ArrayValue, add statistics
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-02 10:55:39 -08:00
Nikolaj Bjorner
bf14aeb1bd
stub out nativesolver
2022-03-02 10:06:38 -08:00
Nikolaj Bjorner
bbadd17d56
fix #5874
2022-03-02 08:46:28 -08:00
Nikolaj Bjorner
5f79a977fb
use conventions from Context
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-01 14:27:57 -08:00
Nikolaj Bjorner
c812d1e890
update native func interp
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-01 14:07:20 -08:00
Nikolaj Bjorner
61d2654770
quantifier
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-01 13:18:18 -08:00
Nikolaj Bjorner
deeb5e9921
finish NativeModel
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-01 12:40:03 -08:00
Nikolaj Bjorner
c0826d58bf
add stubs for native model and func interp
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-01 12:11:10 -08:00
Nikolaj Bjorner
deaad86d6a
nit
2022-03-01 12:11:10 -08:00
Nikolaj Bjorner
2b6dadcbc6
fix #5869
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-28 17:02:13 -08:00
Nikolaj Bjorner
302c0d178c
fix #5867
2022-02-26 09:52:23 -08:00
Clemens Eisenhofer
412b05076c
User-functions fix ( #5868 )
2022-02-26 09:21:01 -08:00
Nuno Lopes
689e2d41de
remove a bunch of unneeded memory allocations
2022-02-25 16:08:23 +00:00
Nikolaj Bjorner
7f149a36d7
refining model update rules for del_rule #5865 #5866
2022-02-25 08:03:46 -08:00
Nikolaj Bjorner
30a2f2fd9d
initial stab at NativeContext
2022-02-25 07:56:36 -08:00
Nikolaj Bjorner
f2e712b0d6
throttle is_compatible to check variables at most once
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-23 08:45:22 -08:00
Nikolaj Bjorner
7b4f1ed530
missing initialization of m_user_propagator, disable unsound in-processing in pb_solver
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-23 04:49:42 -08:00
Nikolaj Bjorner
6be0a66b38
fix #5863
2022-02-22 13:00:20 -08:00
Nikolaj Bjorner
6af170b058
fix #5861
...
sigh
2022-02-22 11:26:09 -08:00
Nikolaj Bjorner
c2f1bdc099
fix #5862
2022-02-22 08:05:05 -08:00
Nikolaj Bjorner
11030fc81d
disable unsound mk_seq_butlast
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-21 18:56:49 -08:00
Nikolaj Bjorner
ea0876b6d6
add lambda definitions during ast translation #5820
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-21 18:05:29 -08:00
Nikolaj Bjorner
d06c51d517
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-21 17:46:54 -08:00
Nikolaj Bjorner
061e94d723
#5858
...
COI model converter has to use constraints from the body and work in disjunctive mode. It needs a pre-condition that the body does not depend on other rules, in the case that it is used in a different pre-processing step for in-lining. The in-lined occurrence of the predicate has to correspond to the model construction version.
2022-02-21 17:45:00 -08:00
Nikolaj Bjorner
e8d4804dbb
Revert "use horn_subsume_model_converter in coi filter ( #5844 )" ( #5859 )
...
This reverts commit 09da87dc85
2022-02-21 04:33:52 -08:00
Nikolaj Bjorner
b843618051
fix #5798
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-20 13:54:15 -08:00
Nikolaj Bjorner
5c2624950b
#5849
2022-02-20 09:52:42 -08:00
Nikolaj Bjorner
1e463955c2
#4889 avoid double internalize of bvle
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-20 09:09:28 -08:00
Nikolaj Bjorner
f66b4f0880
fir #5856
2022-02-20 15:32:41 +02:00
Nikolaj Bjorner
d0d4ab7955
#5820
2022-02-20 10:33:29 +02:00
Nikolaj Bjorner
ff5d210e81
na
2022-02-20 10:33:15 +02:00
Nikolaj Bjorner
4d184fe65d
skip expensive equality rewriting of Booleans
2022-02-20 10:31:10 +02:00
Nikolaj Bjorner
10b611b3ba
fix #5850
2022-02-20 10:30:52 +02:00
Nikolaj Bjorner
91045d3e4a
two words
2022-02-20 10:29:57 +02:00
Nikolaj Bjorner
9a1a72867c
Add str.<= and str.< to Java API
2022-02-20 10:29:38 +02:00
Nikolaj Bjorner
7091b1c856
add additional regex operators to API
2022-02-20 10:29:18 +02:00
Nikolaj Bjorner
2e00f2f32d
Propagator ( #5845 )
...
* user propagator without ids
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* user propagator without ids
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix signature
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* references #5818
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix c++ build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch to vs 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Update propagator example (I) (#5835 )
* fix #5829
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch to vs 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Adapted the example to the changes in the propagator
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* context goes out of scope in stack allocation, so can't used scoped context when passing objects around
* parameter check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Fixed bug in user-propagator "created" (#5843 )
Co-authored-by: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
2022-02-17 09:21:41 +02:00
mbergen
2e15e2aa4d
Add access to builtin special relations (Context::mkLinearOrder and Context::mkPartialOrder ) to Java API ( #5832 )
...
* Add mkLinearOrder
* reorder arguments to match definition, add short comment
* add partial order
* add comments
2022-02-16 23:37:20 +02:00
Qix
9cf50766a6
fix compiler warnings under clang ( #5839 )
2022-02-16 23:36:34 +02:00
Valentine Sobol
09da87dc85
use horn_subsume_model_converter in coi filter ( #5844 )
2022-02-16 23:35:58 +02:00
Nikolaj Bjorner
5bbb8fb807
add bail #5825
2022-02-16 23:30:12 +02:00
Nikolaj Bjorner
33985ebcf5
update expected
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-16 19:14:54 +02:00
Nikolaj Bjorner
6202cd5394
fix #5842
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-16 17:38:19 +02:00
Nikolaj Bjorner
aa6ec418e3
move idiv test to after cuts/branch
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-14 19:50:49 +02:00
Nikolaj Bjorner
9a4d6cee6c
overhead with push-ite on shared terms
2022-02-14 19:36:14 +02:00
Nikolaj Bjorner
3d26b501e7
fix #5827 #5828
2022-02-14 10:31:04 +02:00
Nikolaj Bjorner
81e94b2154
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-09 12:10:01 +02:00
