From 442b8f2c7070321aa167d9454f92bd1be88fe0cc Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 1 Nov 2014 16:05:49 +0100
Subject: [PATCH] Fix cegqi for synthesis without syntax.

---
 .../quantifiers/ce_guided_instantiation.cpp      | 16 +++++++++++++---
 src/theory/quantifiers/ce_guided_instantiation.h |  2 ++
 2 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 2ec15f538..5c7b31d33 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -47,6 +47,12 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){
     d_guard = qe->getValuation().ensureLiteral( d_guard );
     AlwaysAssert( !d_guard.isNull() );
     qe->getOutputChannel().requirePhase( d_guard, true );
+    if( !d_syntax_guided ){
+      //add immediate lemma
+      Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), d_base_inst.negate() );
+      Trace("cegqi") << "Add candidate lemma : " << lem << std::endl;
+      qe->getOutputChannel().lemma( lem );
+    }
   }
 }
 
@@ -109,10 +115,11 @@ void CegInstantiation::registerQuantifier( Node q ) {
         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 ) ){
-        //add immediate lemma
-        Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_base_inst );
-        d_quantEngine->getOutputChannel().lemma( lem );
+        d_conj->d_syntax_guided = false;
+      }else{
+        Assert( false );
       }
       //fairness
       if( options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){
@@ -233,11 +240,14 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       }
 
     }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
+      Trace("cegqi-engine") << "  * Value is : ";
       std::vector< Node > model_terms;
       for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
         Node t = getModelTerm( conj->d_candidates[i] );
         model_terms.push_back( t );
+        Trace("cegqi-engine") << t << " ";
       }
+      Trace("cegqi-engine") << std::endl;
       d_quantEngine->addInstantiation( q, model_terms, false );
     }
   }else{
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 2502416bd..67125a8ad 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -44,6 +44,8 @@ private:
     Node d_base_inst;
     /** guard split */
     Node d_guard_split;
+    /** is syntax-guided */
+    bool d_syntax_guided;
     /** list of constants for quantified formula */
     std::vector< Node > d_candidates;
     /** list of variables on inner quantification */
-- 
2.30.2