Add option to minimize sygus solutions based on using weakest implicants of instantia...

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 37178510dcf9b3ae86ee1227b29c0c2a86adfe29..953150e425546ead83963ef67d9b45205dc0523e 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -244,6 +244,8 @@ option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
   reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSolMinCore --cegqi-si-sol-min-core bool :default false
   minimize solutions for single invocation conjectures based on unsat core
+option cegqiSolMinInst --cegqi-si-sol-min-inst bool :default true
+  minimize individual instantiations for single invocation conjectures based on unsat core
 option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true
   include constants when reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 3f781774de6a6762751ad91527885387153f13bc..981abea944863b43ce8264df1efd3c5a3c18bc76 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -658,7 +658,7 @@ bool CegConjectureSingleInv::check( std::vector< Node >& lems ) {
   }
 }
 
-Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index ) {
+Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index, std::map< Node, Node >& weak_imp ) {
   Assert( index<d_inst.size() );
   Assert( i<d_inst[index].size() );
   unsigned uindex = indices[index];
@@ -666,9 +666,14 @@ Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices
     return d_inst[uindex][i];
   }else{
     Node cond = d_lemmas_produced[uindex];
+    //weaken based on unsat core
+    std::map< Node, Node >::iterator itw = weak_imp.find( cond );
+    if( itw!=weak_imp.end() ){
+      cond = itw->second;
+    }
     cond = TermDb::simpleNegate( cond );
     Node ite1 = d_inst[uindex][i];
-    Node ite2 = constructSolution( indices, i, index+1 );
+    Node ite2 = constructSolution( indices, i, index+1, weak_imp );
     return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 );
   }
 }
@@ -756,8 +761,17 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
     bool useUnsatCore = false;
     std::vector< Node > active_lemmas;
     //minimize based on unsat core, if possible
-    if( options::cegqiSolMinCore() && d_qe->getUnsatCoreLemmas( active_lemmas ) ){
-      useUnsatCore = true;
+    std::map< Node, Node > weak_imp;
+    if( options::cegqiSolMinCore() ){
+      if( options::cegqiSolMinInst() ){
+        if( d_qe->getUnsatCoreLemmas( active_lemmas, weak_imp ) ){
+          useUnsatCore = true;
+        }
+      }else{
+        if( d_qe->getUnsatCoreLemmas( active_lemmas ) ){
+          useUnsatCore = true;
+        }
+      }
     } 
     Assert( d_lemmas_produced.size()==d_inst.size() );
     std::vector< unsigned > indices;
@@ -780,7 +794,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
     ssii.d_i = sol_index;
     std::sort( indices.begin(), indices.end(), ssii );
     Trace("csi-sol") << "Construct solution" << std::endl;
-    s = constructSolution( indices, sol_index, 0 );
+    s = constructSolution( indices, sol_index, 0, weak_imp );
     Assert( vars.size()==d_sol->d_varList.size() );
     s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() );
   }

diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 4d2f9a0e59a2569cc34bd9a7c8e946324980219f..feadeca393bd2a75f7dc5d32ecc8b038a4e6ad1a 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -74,7 +74,7 @@ private:
                                std::map< Node, std::vector< Node > >& teq,
                                Node n, std::vector< Node >& conj );
   //constructing solution
-  Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index );
+  Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index, std::map< Node, Node >& weak_imp );
   Node postProcessSolution( Node n );
 private:
   //list of skolems for each argument of programs

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2975d2e704d2cd85d1ea29d370405c0b8f053952..75d177fdc577297f33e0d87307fd3475bb8c127d 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1307,6 +1307,21 @@ bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas )
   }
 }
 
+bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ) {
+  if( getUnsatCoreLemmas( active_lemmas ) ){
+    for (unsigned i = 0; i < active_lemmas.size(); ++i) {
+      Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore(active_lemmas[i]);
+      if( n!=active_lemmas[i] ){
+        Trace("inst-unsat-core") << "  weaken : " << active_lemmas[i] << " -> " << n << std::endl;
+      }
+      weak_imp[active_lemmas[i]] = n;
+    }
+    return true;
+  }else{
+    return false;
+  }
+}
+
 void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) {
   if( d_trackInstLemmas ){
     if( options::incrementalSolving() ){

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 1ba0b657283f8e705cbd898258c6798023e2dce8..08ca0564bf8497a00e91341e6224bd0634e9b9c3 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -368,6 +368,7 @@ public:
   void getInstantiations( std::map< Node, std::vector< Node > >& insts );
   /** get unsat core lemmas */
   bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas );
+  bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp );
   /** get inst for lemmas */
   void getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ); 
   /** statistics class */