Arie Gurfinkel
cdba0721e7
Extra stats in iuc_solver
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
16fefe850a
Factored mbp into pred_transformer and added stats
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
fde58664f6
Moved mk_reach_fact to pred_transformer
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
2a2b21326b
Stats on num_proxies in iuc_solver
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
e2e1411707
Option to dump SMT queries as benchmarks during Spacer run
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
bebfac047e
Dump benchmarks in pool_solver
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
b50da20531
array_mbp: turn on model completion
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
0452bc3d43
qe_lite: simplify definitions before deciding on elimination order
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
b120923dd5
qe_lite: bug fix in der::der_sort_vars()
...
The case of
VAR 1 = (+ (:var 2) 10)
VAR 2 = (+ 0 foo)
was not properly handled whenever VAR2 has only one reference.
In that case, VAR2 is not marked as done when VAR1 is processed,
causing VAR2 to be duplicated in elimination order
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
fb52c36210
spacer: switch to new IUC as default
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
3a97451f8c
spacer: normalize the cube before creating a lemma
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
fce68536d3
spacer: print all lemmas in json
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
bfa472faec
New style of json dump based on lemmas at pob
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
5072a2a869
spacer: pobs keep track of their lemmas
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
61cd74818f
Pin lemmas so that they don't disappear
2018-06-14 16:08:50 -07:00
Nikolaj Bjorner
ebfb2a4a1e
Fix mbp to respect reduce_all_selects option
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:50 -07:00
Nikolaj Bjorner
0c2e3c0894
fixes to clause proof tracking
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
f7d015de8d
Switch spacer_prop_solver to check_sat_cc
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
1343b272e7
Implement iuc_solver::check_sat_cc
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
26339119e4
solver::check_sat_cc : check_sat assuming cube and clause
...
Extends check_sat with an ability to assume a single clause in
addition to assuming a cube of assumptions
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
4477f7d326
Fix memory leak in asserted_formulas
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
723e96175b
spacer: prepare to use incremental clause smt_solver interface
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
c3edf8c8fa
Restore assertion in smt_clause
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
ef58753ae7
Silence clang warning
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
56a29093d0
Cleanup transition creation in pred_transformer
2018-06-14 16:08:50 -07:00
Nikolaj Bjorner
005a6d93bb
cube and clause
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
ea032b56c0
Return false when clause cannot be decided
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
275b99e408
Add missing override
2018-06-14 16:08:50 -07:00
Arie Gurfinkel
4db4547359
silence clang warning
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
b73aa3642a
check with cube and clause
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
af57db0413
Anti-unification of two ground expressions
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
aa8dac2583
fix uninitialized variable
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
e6401908a5
fix crash
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
a8438e081e
Wired qe::mbp into spacer
...
use option fixedpoint.spacer.native_mbp=true to use it
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
7e9f7d2cfe
remove removed paramter from comment
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
92bac11778
update to make variables work with other theories
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
5eacb8122d
add tuple features, remove dead code from mbp
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
560a26127e
bind nested variables
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
692a701516
updates to mbp
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
7642106e73
add way to unit test mbp from command line
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
20300bbf94
updates to mbqi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
80c39eb037
Fix solver_pool::updt_params
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
14b9dd2cd7
spacer: let pool_solver own the solver
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
15d0fd4b42
spacer: removed virtual_solver
...
This commit removes virtual_solver and smt_context_manager that have
been migrated into solver_pool
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
098e70a9e2
spacer: switched to using solver_pool
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
180d38378a
Add additional API to solver_pool
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
c2304e2636
spacer: Cleanup of smt parameter configuration
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
b17be763d3
User control over more arith options
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
cfeee55d4f
spacer: set qi.quick_checker to MC_UNSAT if quantifiers are expected
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
c8187886cf
spacer: use same params for all solver pools
2018-06-14 16:08:49 -07:00
