diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-29 18:24:43 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-29 18:24:43 -0600 |
| commit | 47d542f312ac8e22e8d3aae1007cfd13701983a6 (patch) | |
| tree | 5d1f0062fa535f5f64528ff3e2b110e7456f2f52 /src/theory/quantifiers/ceg_instantiator.cpp | |
| parent | 0b821fa27929b5a65ce78767d26a21f779a82d3d (diff) | |
Cbqi repeat solve literal (#1458)
Diffstat (limited to 'src/theory/quantifiers/ceg_instantiator.cpp')
| -rw-r--r-- | src/theory/quantifiers/ceg_instantiator.cpp | 31 |
1 files changed, 28 insertions, 3 deletions
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; |