mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

spacer: prepare to use incremental clause smt_solver interface

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-28 18:28:59 -07:00
parent c3edf8c8fa
commit 723e96175b
4 changed files with 45 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/muz/base/fixedpoint_params.pyg
View file

@ -4,7 +4,7 @@ def_module_params('fixedpoint',
params=(('timeout', UINT, UINT_MAX, 'set timeout'),
('engine', SYMBOL, 'auto-config',
'Select: auto-config, datalog, spacer, pdr, bmc'),
('datalog.default_table', SYMBOL, 'sparse',
('datalog.default_table', SYMBOL, 'sparse',
'default table implementation: sparse, hashtable, bitvector, interval'),
('datalog.default_relation', SYMBOL, 'pentagon',
'default relation implementation: external_relation, pentagon'),
@ -80,9 +80,9 @@ def_module_params('fixedpoint',
"generalize lemmas using induction strengthening"),
('pdr.use_arith_inductive_generalizer', BOOL, False,
"generalize lemmas using arithmetic heuristics for induction strengthening"),
('pdr.use_convex_closure_generalizer', BOOL, False,
('pdr.use_convex_closure_generalizer', BOOL, False,
"generalize using convex closures of lemmas"),
('pdr.use_convex_interior_generalizer', BOOL, False,
('pdr.use_convex_interior_generalizer', BOOL, False,
"generalize using convex interiors of lemmas"),
('pdr.cache_mode', UINT, 0, "use no (0), symbolic (1) or explicit " +
"cache (2) for model search"),
@ -92,7 +92,7 @@ def_module_params('fixedpoint',
('pdr.max_num_contexts', UINT, 500, "maximal number of contexts to create"),
('pdr.try_minimize_core', BOOL, False,
"try to reduce core size (before inductive minimization)"),
('pdr.utvpi', BOOL, True, 'Enable UTVPI strategy'),
('pdr.utvpi', BOOL, True, 'Enable UTVPI strategy'),
('print_fixedpoint_extensions', BOOL, True,
"use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, " +
"when printing rules"),
@ -111,7 +111,7 @@ def_module_params('fixedpoint',
('print_statistics', BOOL, False, 'print statistics'),
('print_aig', SYMBOL, '',
'Dump clauses in AIG text format (AAG) to the given file name'),
('tab.selection', SYMBOL, 'weight',
('tab.selection', SYMBOL, 'weight',
'selection method for tabular strategy: weight (default), first, var-use'),
('xform.bit_blast', BOOL, False,
'bit-blast bit-vectors'),
@ -128,7 +128,7 @@ def_module_params('fixedpoint',
('xform.unfold_rules', UINT, 0,
"unfold rules statically using iterative squarring"),
('xform.slice', BOOL, True, "simplify clause set using slicing"),
('xform.karr', BOOL, False,
('xform.karr', BOOL, False,
"Add linear invariants to clauses using Karr's method"),
('spacer.use_eqclass', BOOL, False, "Generalizes equalities to equivalence classes"),
('xform.transform_arrays', BOOL, False,
@ -141,9 +141,9 @@ def_module_params('fixedpoint',
"Gives the number of quantifiers per array"),
('xform.instantiate_arrays.slice_technique', SYMBOL, "no-slicing",
"<no-slicing>=> GetId(i) = i, <smash> => GetId(i) = true"),
('xform.quantify_arrays', BOOL, False,
('xform.quantify_arrays', BOOL, False,
"create quantified Horn clauses from clauses with arrays"),
('xform.instantiate_quantifiers', BOOL, False,
('xform.instantiate_quantifiers', BOOL, False,
"instantiate quantified Horn clauses using E-matching heuristic"),
('xform.coalesce_rules', BOOL, False, "coalesce rules"),
('xform.tail_simplifier_pve', BOOL, True, "propagate_variable_equivalences"),
@ -155,9 +155,9 @@ def_module_params('fixedpoint',
('spacer.reset_obligation_queue', BOOL, True, 'SPACER: reset obligation queue when entering a new level'),
('spacer.init_reach_facts', BOOL, True, 'SPACER: initialize reachability facts with false'),
('spacer.use_array_eq_generalizer', BOOL, True, 'SPACER: attempt to generalize lemmas with array equalities'),
('spacer.use_derivations', BOOL, True, 'SPACER: using derivation mechanism to cache intermediate results for non-linear rules'),
('spacer.use_derivations', BOOL, True, 'SPACER: using derivation mechanism to cache intermediate results for non-linear rules'),
('xform.array_blast', BOOL, False, "try to eliminate local array terms using Ackermannization -- some array terms may remain"),
('xform.array_blast_full', BOOL, False, "eliminate all local array variables by QE"),
('xform.array_blast_full', BOOL, False, "eliminate all local array variables by QE"),
('spacer.skip_propagate', BOOL, False, "Skip propagate/pushing phase. Turns PDR into a BMC that returns either reachable or unknown"),
('spacer.max_level', UINT, UINT_MAX, "Maximum level to explore"),
('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"),
@ -202,4 +202,5 @@ def_module_params('fixedpoint',
('spacer.from_level', UINT, 0, 'starting level to explore'),
('spacer.print_json', SYMBOL, '', 'print pobs tree in JSON format to a given file'),
('spacer.ctp', BOOL, False, 'enable counterexample-to-pushing technique'),
('spacer.use_inc_clause', BOOL, False, 'Use incremental clause to represent trans'),
))

31
src/muz/spacer/spacer_context.cpp
View file

@ -1199,9 +1199,13 @@ bool pred_transformer::is_blocked (pob &n, unsigned &uses_level)
m_solver.set_core (nullptr);
m_solver.set_model (nullptr);
expr_ref_vector post(m), aux(m);
expr_ref_vector post(m), _aux(m);
post.push_back (n.post ());
lbool res = m_solver.check_assumptions (post, aux, 0, nullptr, 0);
// this only uses the lemmas at the current level
// transition relation is irrelevant
// XXX quic3: not all lemmas are asserted at the post-condition
lbool res = m_solver.check_assumptions (post, _aux, _aux,
0, nullptr, 0);
if (res == l_false) { uses_level = m_solver.uses_level(); }
return res == l_false;
}
@ -1315,7 +1319,8 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
// result is either sat (with some reach assumps) or
// unsat (even with no reach assumps)
expr *bg = m_extend_lit.get ();
lbool is_sat = m_solver.check_assumptions (post, reach_assumps, 1, &bg, 0);
lbool is_sat = m_solver.check_assumptions (post, reach_assumps,
m_transition_clause, 1, &bg, 0);
TRACE ("spacer",
if (!reach_assumps.empty ()) {
@ -1423,7 +1428,8 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem,
m_solver.set_core(core);
m_solver.set_model(mdl_ref_ptr);
expr * bg = m_extend_lit.get ();
lbool r = m_solver.check_assumptions (conj, aux, 1, &bg, 1);
lbool r = m_solver.check_assumptions (conj, aux, m_transition_clause,
1, &bg, 1);
if (r == l_false) {
solver_level = m_solver.uses_level ();
lem->reset_ctp();
@ -1455,7 +1461,9 @@ bool pred_transformer::check_inductive(unsigned level, expr_ref_vector& state,
m_solver.set_model (nullptr);
expr_ref_vector aux (m);
conj.push_back (m_extend_lit);
lbool res = m_solver.check_assumptions (state, aux, conj.size (), conj.c_ptr (), 1);
lbool res = m_solver.check_assumptions (state, aux,
m_transition_clause,
conj.size (), conj.c_ptr (), 1);
if (res == l_false) {
state.reset();
state.append(core);
@ -1557,8 +1565,10 @@ void pred_transformer::init_rules(decl2rel const& pts) {
m_transition_clause.push_back(m_extend_lit->get_arg(0));
m_transition_clause.push_back(tag);
transitions.push_back(mk_or(m_transition_clause));
m_transition_clause.reset();
if (!ctx.get_params().spacer_use_inc_clause()) {
transitions.push_back(mk_or(m_transition_clause));
m_transition_clause.reset();
}
if (!is_init[0]) {init_conds.push_back(m.mk_not(tag));}
@ -1577,8 +1587,11 @@ void pred_transformer::init_rules(decl2rel const& pts) {
// update init conds
if (!is_init[i]) {init_conds.push_back (m.mk_not (tag));}
}
transitions.push_back(mk_or(m_transition_clause));
m_transition_clause.reset();
if (!ctx.get_params().spacer_use_inc_clause()) {
transitions.push_back(mk_or(m_transition_clause));
m_transition_clause.reset();
}
m_transition = mk_and(transitions);
break;
}

12
src/muz/spacer/spacer_prop_solver.cpp
View file

@ -347,9 +347,13 @@ lbool prop_solver::internal_check_assumptions(
lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
expr_ref_vector& soft,
const expr_ref_vector &clause,
unsigned num_bg, expr * const * bg,
unsigned solver_id)
{
expr_ref cls(m);
// XXX now clause is only supported when pushing is enabled
SASSERT(clause.empty() || !m_use_push_bg);
// current clients expect that flattening of HARD is
// done implicitly during check_assumptions
expr_ref_vector hard(m);
@ -360,7 +364,13 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
// can be disabled if use_push_bg == true
// solver::scoped_push _s_(*m_ctx);
if (!m_use_push_bg) { m_ctx->push(); }
if (!m_use_push_bg) {
m_ctx->push();
if (!clause.empty()) {
cls = mk_or(clause);
m_ctx->assert_expr(cls);
}
}
iuc_solver::scoped_bg _b_(*m_ctx);
for (unsigned i = 0; i < num_bg; ++i)

1
src/muz/spacer/spacer_prop_solver.h
View file

@ -94,6 +94,7 @@ public:
*/
lbool check_assumptions(const expr_ref_vector & hard,
expr_ref_vector & soft,
const expr_ref_vector &clause,
unsigned num_bg = 0,
expr * const *bg = nullptr,
unsigned solver_id = 0);