Cbqi repeat solve literal (#1458)

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 65731547dd7f46666d9629f69b893a10814c75e2..27671fd82dfe163b8481389043dc09222b8b9e5b 100644 (file)
--- 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 78cd77c6ecea8f660b1ace428fce5fe882db5ca4..e14ae78fc773b2d1226358e86d7390a4b2a93995 100644 (file)
--- 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 126f0325ffd25b444f19799fe42c56decc058eea..a0137abde35453f438ae8416041e337f8d36eb8a 100644 (file)
--- 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<Node, std::vector<Node> > d_curr_eqc;
   /** map from types to representatives of that type */
   std::map<TypeNode, std::vector<Node> > d_curr_type_eqc;
+  /** solved asserts */
+  std::unordered_set<Node, NodeHashFunction> 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 8a0412a800257fed59dbe487a57af589bcd6184d..f0031cd54b099df43cf84f2dc3979f37eac1b689 100644 (file)
--- 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)
       {