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
Arie Gurfinkel
1c06229755
User control over qi.quick_checker smt_params option
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
d06f4bd337
Fix reset of params_ref in solver
...
params_ref is not a ref, and params_ref::reset is not ref::reset.
params_ref::reset resets the params object being pointed to by
params_ref.
A proper way to reset a params_ref as a reference is to assign an
empty params_ref object to it.
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
ec8a86b78a
Removed unused m_qi_ematching parameter from smt_params
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
c2b8f25cf9
Switch to using solver instead of smt::kernel all around
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
4b09cefb97
Replace smt::kernel with smt_solver
...
Replace all ad-hoc uses of smt::kernel with ad-hoc uses of smt_solver
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
df2e9d8fe2
Make smt_solver::updt_params() commulative
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
9c37bef553
Fix bug in ctp
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
1da002d7b1
scoped params on solver
...
solver::push_params() saves current parameters
solver::pop_params() restores previously saved parameters
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
477ac4a19a
Remove dead m_propagate_booleans param
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
40781c0b0c
Comment on params used in spacer_context
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
55126692c9
spacer: counterexample to pushing (ctp)
...
Enable using fixedpoint.spacer.ctp=true
For each lemma L currently at level k, keep a model M that justifies
why L cannot be pushed to (k+1). L is not pushed while the model M
remains valid.
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
95d820196b
Cleanup
2018-06-14 16:08:49 -07:00
Arie Gurfinkel
68b7966254
Use C++11
2018-06-14 16:08:49 -07:00
