Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding declare-var vs synth-fun arguments. Handle ground properties in sythesis conjectures.

4 files changed, 35 insertions, 16 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 1b02b2a13..e6dce35e0 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -28,7 +28,7 @@ using namespace std;
 namespace CVC4 {
 
 CegInstantiation::CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
-
+  d_refine_count = 0;
 }
 
 void CegInstantiation::CegConjecture::assign( Node q ) {
@@ -113,10 +113,10 @@ void CegInstantiation::registerQuantifier( Node q ) {
       d_conj->d_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj->d_candidates ) );
       Trace("cegqi") << "Base instantiation is : " << d_conj->d_base_inst << std::endl;
       if( getTermDatabase()->isQAttrSygus( q ) ){
-        Assert( d_conj->d_base_inst.getKind()==NOT );
-        Assert( d_conj->d_base_inst[0].getKind()==FORALL );
-        for( unsigned j=0; j<d_conj->d_base_inst[0][0].getNumChildren(); j++ ){
-          d_conj->d_inner_vars.push_back( d_conj->d_base_inst[0][0][j] );
+        if( d_conj->d_base_inst.getKind()==NOT && d_conj->d_base_inst[0].getKind()==FORALL ){
+          for( unsigned j=0; j<d_conj->d_base_inst[0][0].getNumChildren(); j++ ){
+            d_conj->d_inner_vars.push_back( d_conj->d_base_inst[0][0][j] );
+          }
         }
         d_conj->d_syntax_guided = true;
       }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
@@ -230,14 +230,18 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
           //must get a counterexample to the value of the current candidate
           Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
           inst = Rewriter::rewrite( inst );
-          //body should be an existential
-          Assert( inst.getKind()==NOT );
-          Assert( inst[0].getKind()==FORALL );
-          //immediately skolemize
-          Node inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] ).negate();
+          //if body is existential, immediately skolemize
+          Node inst_sk;
+          if( inst.getKind()==NOT && inst[0].getKind()==FORALL ){
+            inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] ).negate();
+          }else{
+            inst_sk = inst;
+          }
           Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl;
           d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk ) );
-          conj->d_ce_sk.push_back( inst[0] );
+          if( !conj->isGround() || conj->d_refine_count==0 ){
+            conj->d_ce_sk.push_back( inst[0] );
+          }
           Trace("cegqi-engine") << "  ...find counterexample." << std::endl;
         }
       }
@@ -261,12 +265,18 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       std::vector< Node > model_values;
       if( getModelValues( getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){
         //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate
-        Node inst_ce_refine = conj->d_base_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(),
-                                                                  model_values.begin(), model_values.end() );
+        Node inst_ce_refine;
+        if( !conj->d_inner_vars.empty() ){
+          inst_ce_refine = conj->d_base_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(),
+                                                               model_values.begin(), model_values.end() );
+        }else{
+          inst_ce_refine = conj->d_base_inst.negate();
+        }
         Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine );
         Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl;
         Trace("cegqi-engine") << "  ...refine candidate." << std::endl;
         d_quantEngine->addLemma( lem );
+        conj->d_refine_count++;
       }
     }
     conj->d_ce_sk.clear();
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 235f2b01c..4f44c121f 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -56,6 +56,8 @@ private:
     Node d_measure_term;
     /** measure sum size */
     int d_measure_term_size;
+    /** refine count */
+    unsigned d_refine_count;
     /** assign */
     void assign( Node q );
     /** is assigned */
@@ -69,6 +71,8 @@ private:
     context::CDO< int > d_curr_lit;
     /** allocate literal */
     Node getLiteral( QuantifiersEngine * qe, int i );
+    /** is ground */
+    bool isGround() { return d_inner_vars.empty(); }
   };
   /** the quantified formula stating the synthesis conjecture */
   CegConjecture * d_conj;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index e04e76835..fc59b22b7 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -196,6 +196,10 @@ option ceGuidedInst --cegqi bool :default false :read-write
   counterexample-guided quantifier instantiation
 option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h"
   if and how to apply fairness for cegqi
+option sygusMinGrammar --sygus-min-grammar bool :default false
+  minimize sygus grammars
+option sygusDecompose --sygus-decompose bool :default false
+  decompose single invocation synthesis conjectures
  
 
 option localTheoryExt --local-t-ext bool :default false
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index be58919db..efa12b893 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1158,9 +1158,10 @@ void TermDb::computeAttributes( Node q ) {
           d_fun_defs[f] = true;
         }
         if( avar.getAttribute(SygusAttribute()) ){
-          //should be nested existential
-          Assert( q[1].getKind()==NOT );
-          Assert( q[1][0].getKind()==FORALL );
+          //not necessarily nested existential
+          //Assert( q[1].getKind()==NOT );
+          //Assert( q[1][0].getKind()==FORALL );
+          
           Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
           d_qattr_sygus[q] = true;
           if( d_quantEngine->getCegInstantiation()==NULL ){