From 47d542f312ac8e22e8d3aae1007cfd13701983a6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 29 Dec 2017 18:24:43 -0600 Subject: [PATCH] Cbqi repeat solve literal (#1458) --- src/options/quantifiers_options | 2 ++ src/theory/quantifiers/ceg_instantiator.cpp | 31 +++++++++++++++++-- src/theory/quantifiers/ceg_instantiator.h | 6 ++++ src/theory/quantifiers/ceg_t_instantiator.cpp | 5 ++- 4 files changed, 40 insertions(+), 4 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 65731547d..27671fd82 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -311,6 +311,8 @@ option cbqiAll --cbqi-all bool :read-write :default false apply counterexample-based instantiation to all quantified formulas option cbqiMultiInst --cbqi-multi-inst bool :read-write :default false when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation +option cbqiRepeatLit --cbqi-repeat-lit bool :read-write :default false + solve literals more than once in counterexample-based quantifier instantiation # CEGQI for arithmetic option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 78cd77c6e..e14ae78fc 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -427,8 +427,12 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) Node lit = ita->second[j]; if( lits.find(lit)==lits.end() ){ lits.insert(lit); - Node plit = - vinst->hasProcessAssertion(this, sf, pv, lit, d_effort); + Node plit; + if (options::cbqiRepeatLit() || !isSolvedAssertion(lit)) + { + plit = + vinst->hasProcessAssertion(this, sf, pv, lit, d_effort); + } if (!plit.isNull()) { Trace("cbqi-inst-debug2") << " look at " << lit; if (plit != lit) { @@ -438,9 +442,12 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) // apply substitutions Node slit = applySubstitutionToLiteral(plit, sf); if( !slit.isNull() ){ - Trace("cbqi-inst-debug") << "...try based on literal " << slit << std::endl; // check if contains pv if( hasVariable( slit, pv ) ){ + Trace("cbqi-inst-debug") << "...try based on literal " + << slit << "," << std::endl; + Trace("cbqi-inst-debug") << "...from " << lit + << std::endl; if (vinst->processAssertion( this, sf, pv, slit, lit, d_effort)) { @@ -860,6 +867,7 @@ bool CegInstantiator::check() { SolvedForm sf; d_stack_vars.clear(); d_bound_var_index.clear(); + d_solved_asserts.clear(); //try to add an instantiation if (constructInstantiation(sf, 0)) { @@ -1142,6 +1150,23 @@ Node CegInstantiator::getBoundVariable(TypeNode tn) return d_bound_var[tn][index]; } +bool CegInstantiator::isSolvedAssertion(Node n) const +{ + return d_solved_asserts.find(n) != d_solved_asserts.end(); +} + +void CegInstantiator::markSolved(Node n, bool solved) +{ + if (solved) + { + d_solved_asserts.insert(n); + } + else if (isSolvedAssertion(n)) + { + d_solved_asserts.erase(n); + } +} + void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) { if( n.getKind()==FORALL ){ d_is_nested_quant = true; diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 126f0325f..a0137abde 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -269,6 +269,10 @@ class CegInstantiator { * constructing instantiations that involve choice expressions. */ Node getBoundVariable(TypeNode tn); + /** has this assertion been marked as solved? */ + bool isSolvedAssertion(Node n) const; + /** marked solved */ + void markSolved(Node n, bool solved = true); //------------------------------end interface for instantiators /** @@ -328,6 +332,8 @@ class CegInstantiator { std::map > d_curr_eqc; /** map from types to representatives of that type */ std::map > d_curr_type_eqc; + /** solved asserts */ + std::unordered_set d_solved_asserts; /** process assertions * This is called once at the beginning of check to * set up all necessary information for constructing instantiations, diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 8a0412a80..f0031cd54 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -1219,20 +1219,23 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, bool ret = false; bool revertOnSuccess = inst_ids_try.size() > 1; for (unsigned j = 0; j < inst_ids_try.size(); j++) { - unsigned inst_id = iti->second[j]; + unsigned inst_id = inst_ids_try[j]; Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end()); Node inst_term = d_inst_id_to_term[inst_id]; + Node alit = d_inst_id_to_alit[inst_id]; // try instantiation pv -> inst_term TermProperties pv_prop_bv; Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term << std::endl; d_var_to_curr_inst_id[pv] = inst_id; d_tried_assertion_inst = true; + ci->markSolved(alit); if (ci->constructInstantiationInc( pv, inst_term, pv_prop_bv, sf, revertOnSuccess)) { ret = true; } + ci->markSolved(alit, false); } if (ret) { -- 2.30.2