Option to use sampling for CEGIS (#1555)

1 files changed, 19 insertions, 3 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index dc359d252..38cfb9ba7 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -238,17 +238,33 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
 
 void CegInstantiation::getCRefEvaluationLemmas( CegConjecture * conj, std::vector< Node >& vs, std::vector< Node >& ms, std::vector< Node >& lems ) {
   Trace("sygus-cref-eval") << "Cref eval : conjecture has " << conj->getNumRefinementLemmas() << " refinement lemmas." << std::endl;
-  if( conj->getNumRefinementLemmas()>0 ){
+  unsigned nlemmas = conj->getNumRefinementLemmas();
+  if (nlemmas > 0 || options::cegisSample() != CEGIS_SAMPLE_NONE)
+  {
     Assert( vs.size()==ms.size() );
 
     TermDbSygus* tds = d_quantEngine->getTermDatabaseSygus();
     Node nfalse = d_quantEngine->getTermUtil()->d_false;
     Node neg_guard = conj->getGuard().negate();
-    for( unsigned i=0; i<conj->getNumRefinementLemmas(); i++ ){
+    for (unsigned i = 0; i <= nlemmas; i++)
+    {
+      if (i == nlemmas)
+      {
+        bool addedSample = false;
+        // find a new one by sampling, if applicable
+        if (options::cegisSample() != CEGIS_SAMPLE_NONE)
+        {
+          addedSample = conj->sampleAddRefinementLemma(ms, lems);
+        }
+        if (!addedSample)
+        {
+          return;
+        }
+      }
       Node lem;
       std::map< Node, Node > visited;
       std::map< Node, std::vector< Node > > exp;
-      lem = conj->getRefinementBaseLemma( i );
+      lem = conj->getRefinementLemma(i);
       if( !lem.isNull() ){
         std::vector< Node > lem_conj;
         //break into conjunctions