diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 10e319786..b32f1f586 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -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", "=> GetId(i) = i, => 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'), )) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 109055076..5e2d0f1f4 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -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; } diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 6b29df074..dcbc4bf88 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -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) diff --git a/src/muz/spacer/spacer_prop_solver.h b/src/muz/spacer/spacer_prop_solver.h index e87732e94..e1c62443e 100644 --- a/src/muz/spacer/spacer_prop_solver.h +++ b/src/muz/spacer/spacer_prop_solver.h @@ -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);