Refactor model builder from model engine to quant engine. Work on fairness strategy for CEGQI. Add option for single/multi triggers. Minor cleanup.

1 files changed, 185 insertions, 70 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index f4cdd1a60..babfe3f40 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -27,7 +27,8 @@ using namespace std;
 
 namespace CVC4 {
 
-CegInstantiation::CegConjecture::CegConjecture() {
+CegInstantiation::CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
+
 }
 
 void CegInstantiation::CegConjecture::assign( Node q ) {
@@ -38,6 +39,7 @@ void CegInstantiation::CegConjecture::assign( Node q ) {
     d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) );
   }
 }
+
 void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){
   if( d_guard.isNull() ){
     d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
@@ -47,8 +49,25 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){
   }
 }
 
-CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ), d_conj_active( c, false ), d_conj_infeasible( c, false ), d_guard_assertions( c ) {
+Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
+  std::map< int, Node >::iterator it = d_lits.find( i );
+  if( it==d_lits.end() ){
+    Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, NodeManager::currentNM()->mkConst( Rational( i + d_measure_term_size ) ) );
+    lit = Rewriter::rewrite( lit );
+    d_lits[i] = lit;
+
+    Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() );
+    Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl;
+    qe->getOutputChannel().lemma( lem );
+    qe->getOutputChannel().requirePhase( lit, true );
+    return lit;
+  }else{
+    return it->second;
+  }
+}
 
+CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
+  d_conj = new CegConjecture( d_quantEngine->getSatContext() );
 }
 
 bool CegInstantiation::needsCheck( Theory::Effort e ) {
@@ -58,9 +77,10 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) {
 void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
     Trace("cegqi-engine") << "---Countexample Guided Instantiation Engine---" << std::endl;
-    Trace("cegqi-debug") << "Current conjecture status : " << d_conj_active << " " << d_conj_infeasible << std::endl;
-    if( d_conj_active && !d_conj_infeasible ){
-      checkCegConjecture( &d_conj );
+    Trace("cegqi-engine-debug") << std::endl;
+    Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl;
+    if( d_conj->d_active && !d_conj->d_infeasible ){
+      checkCegConjecture( d_conj );
     }
     Trace("cegqi-engine") << "Finished Countexample Guided Instantiation engine." << std::endl;
   }
@@ -68,24 +88,44 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
 
 void CegInstantiation::registerQuantifier( Node q ) {
   if( d_quantEngine->getOwner( q )==this ){
-    if( !d_conj.isAssigned() ){
+    if( !d_conj->isAssigned() ){
       Trace("cegqi") << "Register conjecture : " << q << std::endl;
-      d_conj.assign( q );
+      d_conj->assign( q );
       //construct base instantiation
-      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;
+      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] );
+        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] );
         }
       }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
         //add immediate lemma
-        Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_base_inst );
+        Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_base_inst );
+        d_quantEngine->getOutputChannel().lemma( lem );
+      }
+      //fairness
+      std::vector< Node > mc;
+      for( unsigned j=0; j<d_conj->d_candidates.size(); j++ ){
+        TypeNode tn = d_conj->d_candidates[j].getType();
+        registerMeasuredType( tn );
+        std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn );
+        if( it!=d_uf_measure.end() ){
+          mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, d_conj->d_candidates[j] ) );
+        }
+      }
+      if( !mc.empty() ){
+        d_conj->d_measure_term = mc.size()==1 ? mc[0] : NodeManager::currentNM()->mkNode( PLUS, mc );
+        d_conj->d_measure_term_size = mc.size();
+        Trace("cegqi") << "Measure term is : " << d_conj->d_measure_term << std::endl;
+        //Node ax = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), d_conj->d_measure_term );
+        //ax = Rewriter::rewrite( ax );
+        //Trace("cegqi-lemma") << "Fairness non-negative axiom : " << ax << std::endl;
+        //d_quantEngine->getOutputChannel().lemma( ax );
       }
     }else{
-      Assert( d_conj.d_quant==q );
+      Assert( d_conj->d_quant==q );
     }
   }
 }
@@ -94,83 +134,113 @@ void CegInstantiation::assertNode( Node n ) {
   Trace("cegqi-debug") << "Cegqi : Assert : " << n << std::endl;
   bool pol = n.getKind()!=NOT;
   Node lit = n.getKind()==NOT ? n[0] : n;
-  if( lit==d_conj.d_guard ){
-    d_guard_assertions[lit] = pol;
-    d_conj_infeasible = !pol;
+  if( lit==d_conj->d_guard ){
+    //d_guard_assertions[lit] = pol;
+    d_conj->d_infeasible = !pol;
   }
-  if( lit==d_conj.d_quant ){
-    d_conj_active = true;
+  if( lit==d_conj->d_quant ){
+    d_conj->d_active = true;
   }
 }
 
 Node CegInstantiation::getNextDecisionRequest() {
-  d_conj.initializeGuard( d_quantEngine );
+  d_conj->initializeGuard( d_quantEngine );
   bool value;
-  if( !d_quantEngine->getValuation().hasSatValue( d_conj.d_guard, value ) ) {
-    if( d_guard_assertions.find( d_conj.d_guard )==d_guard_assertions.end() ){
-      if( d_conj.d_guard_split.isNull() ){
-        Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_guard );
-        d_quantEngine->getOutputChannel().lemma( lem );
+  if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
+    if( d_conj->d_guard_split.isNull() ){
+      Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
+      d_quantEngine->getOutputChannel().lemma( lem );
+    }
+    Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
+    return d_conj->d_guard;
+  }
+  //enforce fairness
+  if( d_conj->isAssigned() ){
+    Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+    if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
+      if( !value ){
+        d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 );
+        lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+        Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl;
+        return lit;
       }
-      Trace("cegqi-debug") << "Decide next on : " << d_conj.d_guard << "..." << std::endl;
-      return d_conj.d_guard;
+    }else{
+      Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl;
+      return lit;
     }
   }
+
   return Node::null();
 }
 
 void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
   Node q = conj->d_quant;
-  Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl;
-  Trace("cegqi-engine-debug") << "  * Candidate program/output : ";
+  Trace("cegqi-engine") << "Synthesis conjecture : " << q << std::endl;
+  Trace("cegqi-engine") << "  * Candidate program/output symbol : ";
   for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
-    Trace("cegqi-engine-debug") << conj->d_candidates[i] << " ";
+    Trace("cegqi-engine") << conj->d_candidates[i] << " ";
   }
-  Trace("cegqi-engine-debug") << std::endl;
-
-  if( getTermDatabase()->isQAttrSygus( q ) ){
-    Trace("cegqi-engine-debug") << "  * Values are : ";
-    bool success = true;
-    std::vector< Node > model_values;
-    for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
-      Node v = getModelValue( conj->d_candidates[i] );
-      model_values.push_back( v );
-      Trace("cegqi-engine-debug") << v << " ";
-      if( v.isNull() ){
-        success = false;
+  Trace("cegqi-engine") << std::endl;
+
+  if( conj->d_ce_sk.empty() ){
+    Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
+    if( getTermDatabase()->isQAttrSygus( q ) ){
+
+      std::vector< Node > model_values;
+      if( getModelValues( conj->d_candidates, model_values ) ){
+        //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] );
+        Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl;
+        d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk.negate() ) );
+        conj->d_ce_sk.push_back( inst[0] );
       }
-    }
-    Trace("cegqi-engine-debug") << std::endl;
 
-    if( success ){
-      //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] );
-      Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl;
-      d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk ) );
-
-      //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate
-      Assert( conj->d_inner_vars.size()==getTermDatabase()->d_skolem_constants[inst[0]].size() );
-      Node inst_ce_refine = conj->d_base_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(),
-                                                                getTermDatabase()->d_skolem_constants[inst[0]].begin(), getTermDatabase()->d_skolem_constants[inst[0]].end() );
-      Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine.negate() );
-      Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl;
-      d_quantEngine->addLemma( lem );
+    }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
+      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 );
+      }
+      d_quantEngine->addInstantiation( q, model_terms, false );
     }
+  }else{
+    Trace("cegqi-engine") << "  *** Refine candidate phase..." << std::endl;
+    for( unsigned j=0; j<conj->d_ce_sk.size(); j++ ){
+      Node ce_q = conj->d_ce_sk[j];
+      Assert( conj->d_inner_vars.size()==getTermDatabase()->d_skolem_constants[ce_q].size() );
+      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 lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine );
+        Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl;
+        d_quantEngine->addLemma( lem );
+      }
+    }
+    conj->d_ce_sk.clear();
+  }
+}
 
-  }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
-    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 );
+bool CegInstantiation::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) {
+  bool success = true;
+  Trace("cegqi-engine") << "  * Value is : ";
+  for( unsigned i=0; i<n.size(); i++ ){
+    Node nv = getModelValue( n[i] );
+    v.push_back( nv );
+    Trace("cegqi-engine") << nv << " ";
+    if( nv.isNull() ){
+      success = false;
     }
-    d_quantEngine->addInstantiation( q, model_terms, false );
   }
+  Trace("cegqi-engine") << std::endl;
+  return success;
 }
 
 Node CegInstantiation::getModelValue( Node n ) {
@@ -210,7 +280,52 @@ Node CegInstantiation::getModelValue( Node n ) {
 }
 
 Node CegInstantiation::getModelTerm( Node n ){
+  //TODO
   return getModelValue( n );
 }
 
+void CegInstantiation::registerMeasuredType( TypeNode tn ) {
+  std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn );
+  if( it==d_uf_measure.end() ){
+    if( tn.isDatatype() ){
+      TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->integerType() );
+      Node op = NodeManager::currentNM()->mkSkolem( "tsize", op_tn, "was created by ceg instantiation to enforce fairness." );
+      d_uf_measure[tn] = op;
+      //cycle through constructors
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+        Node x = NodeManager::currentNM()->mkBoundVar( tn );
+        Node cond = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), x ).negate();
+
+        std::vector< Node > sumc;
+        sumc.push_back( NodeManager::currentNM()->mkConst( Rational(1) ) );
+        for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+          TypeNode tnc = TypeNode::fromType( ((SelectorType)dt[i][j].getSelector().getType()).getRangeType() );
+          if( tnc.isDatatype() ){
+            registerMeasuredType( tnc );
+            sumc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_uf_measure[tnc],
+                                                              NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, dt[i][j].getSelector(), x ) ) );
+          }
+        }
+        Node sum = sumc.size()==1 ? sumc[0] : NodeManager::currentNM()->mkNode( PLUS, sumc );
+        Node eq = NodeManager::currentNM()->mkNode( EQUAL, NodeManager::currentNM()->mkNode( APPLY_UF, d_uf_measure[tn], x ), sum );
+
+        Node ax = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ),
+                                                            NodeManager::currentNM()->mkNode( OR, cond, eq ) );
+        ax = Rewriter::rewrite( ax );
+        Trace("cegqi-lemma") << "Fairness axiom : " << ax << std::endl;
+        d_quantEngine->getOutputChannel().lemma( ax );
+      }
+      //all are non-negative
+      Node x = NodeManager::currentNM()->mkBoundVar( tn );
+      Node ax = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ),
+                                                          NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ),
+                                                                                                 NodeManager::currentNM()->mkNode( APPLY_UF, d_uf_measure[tn], x ) ) );
+      ax = Rewriter::rewrite( ax );
+      Trace("cegqi-lemma") << "Fairness non-negative axiom : " << ax << std::endl;
+      d_quantEngine->getOutputChannel().lemma( ax );
+    }
+  }
+}
+
 }
\ No newline at end of file