Add owner map to better manage QuantifiersModules. Initial infrastructure for cegqi.

12 files changed, 161 insertions, 75 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
new file mode 100644
index 000000000..fec4255b2
--- /dev/null
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file ce_guided_instantiation.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief counterexample guided instantiation class
+ **
+ **/
+
+#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace std;
+
+namespace CVC4 {
+
+CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) {
+
+  
+}
+
+void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
+  //TODO
+}
+
+void CegInstantiation::registerQuantifier( Node q ) {
+  //TODO
+}
+
+void CegInstantiation::assertNode( Node n ) {
+  
+}
+  
+}
\ No newline at end of file
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
new file mode 100644
index 000000000..7861deffa
--- /dev/null
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -0,0 +1,46 @@
+/*********************                                                        */
+/*! \file ce_guided_instantiation.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief counterexample guided instantiation class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CE_GUIDED_INSTANTIATION_H
+#define CE_GUIDED_INSTANTIATION_H
+
+#include "context/cdhashmap.h"
+#include "context/cdchunk_list.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class CegInstantiation : public QuantifiersModule
+{
+public:
+  CegInstantiation( QuantifiersEngine * qe, context::Context* c );
+public:
+  /* Call during quantifier engine's check */
+  void check( Theory::Effort e, unsigned quant_e );
+  /* Called for new quantifiers */
+  void registerQuantifier( Node q );
+  void assertNode( Node n );
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  std::string identify() const { return "CegInstantiation"; }
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 25f15cd78..6a2bd5e2e 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -347,47 +347,3 @@ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
   Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
   return mkRationalNode(qmodel);
 }
-
-
-InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) :
-  InstStrategy( qe ), d_th( th ){
-
-}
-
-bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){
-  //DO_THIS
-  return false;
-}
-
-void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){
-  Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;
-  if( e<2 ){
-    return InstStrategy::STATUS_UNFINISHED;
-  }else if( e==2 ){
-    InstMatch m( f );
-    for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
-      Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
-      if( i.getType().isDatatype() ){
-        Node n = getValueFor( i );
-        Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;
-        m.setValue( j, n);
-      }
-    }
-    //d_quantEngine->addInstantiation( f, m );
-  }
-  return InstStrategy::STATUS_UNKNOWN;
-}
-
-Node InstStrategyDatatypesValue::getValueFor( Node n ){
-  //simply get the ground value for n in the current model, if it exists,
-  //  or return an arbitrary ground term otherwise
-  if( !TermDb::hasInstConstAttr(n) ){
-    return n;
-  }else{
-    return n;
-  }
-}
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 9196b9703..bfc0501dc 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -81,29 +81,6 @@ public:
 };
 
 
-class InstStrategyDatatypesValue : public InstStrategy
-{
-protected:
-  /** calculate if we should process this quantifier */
-  bool calculateShouldProcess( Node f );
-private:
-  /** reference to theory datatypes */
-  datatypes::TheoryDatatypes* d_th;
-  /** get value function */
-  Node getValueFor( Node n );
-public:
-  //constructor
-  InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe );
-  ~InstStrategyDatatypesValue(){}
-  /** reset instantiation */
-  void processResetInstantiationRound( Theory::Effort effort );
-  /** process method, returns a status */
-  int process( Node f, Theory::Effort effort, int e );
-  /** identify */
-  std::string identify() const { return std::string("InstStrategyDatatypesValue"); }
-
-};/* class InstStrategy */
-
 }
 }
 }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 7207ceefb..9c3673bc2 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -215,7 +215,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
       //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
-      if( TermDb::isRewriteRule( n ) ){
+      if( !d_quantEngine->hasOwnership( n, this ) ){
         d_quant_active[n] = false;
       }else if( !d_quantEngine->getModel()->isQuantifierActive( n ) ){
         d_quant_active[n] = false;
@@ -300,7 +300,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
 }
 
 void InstantiationEngine::registerQuantifier( Node f ){
-  if( !TermDb::isRewriteRule( f ) ){
+  if( d_quantEngine->hasOwnership( f, this ) ){
     //Notice() << "do cbqi " << f << " ? " << std::endl;
     if( options::cbqi() ){
       Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 2c9a33388..cbff2b581 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -40,7 +40,7 @@ TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe
 }
 
 bool QModelBuilder::isQuantifierActive( Node f ) {
-  return !TermDb::isRewriteRule( f );
+  return d_qe->hasOwnership( f );
 }
 
 
@@ -382,8 +382,7 @@ QModelBuilderIG::Statistics::~Statistics(){
 }
 
 bool QModelBuilderIG::isQuantifierActive( Node f ){
-  return !TermDb::isRewriteRule( f ) &&
-         ( d_considerAxioms || !d_qe->getTermDatabase()->isQAttrAxiom( f ) ) && d_quant_sat.find( f )==d_quant_sat.end();
+  return d_qe->hasOwnership( f ) && ( d_considerAxioms || !d_qe->getTermDatabase()->isQAttrAxiom( f ) ) && d_quant_sat.find( f )==d_quant_sat.end();
 }
 
 bool QModelBuilderIG::isTermActive( Node n ){
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 872f270e7..5e3c66d9a 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -173,4 +173,8 @@ option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0
  number of ground terms to generate for model filtering
 option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false
  more aggressive merging for universal equality engine, introduces terms
+ 
+option ceGuidedInst --cegqi bool :default false
+  counterexample guided quantifier instantiation
+ 
 endmodule
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index ee4464f87..060994379 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1702,7 +1702,7 @@ Node QuantConflictFind::mkEqNode( Node a, Node b ) {
 //-------------------------------------------------- registration

 

 void QuantConflictFind::registerQuantifier( Node q ) {

-  if( !TermDb::isRewriteRule( q ) ){

+  if( d_quantEngine->hasOwnership( q, this ) ){

     d_quants.push_back( q );

     d_quant_id[q] = d_quants.size();

     Trace("qcf-qregister") << "Register ";

@@ -1839,7 +1839,7 @@ bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
 //-------------------------------------------------- handling assertions / eqc

 

 void QuantConflictFind::assertNode( Node q ) {

-  if( !TermDb::isRewriteRule( q ) ){

+  if( d_quantEngine->hasOwnership( q, this ) ){

     Trace("qcf-proc") << "QCF : assertQuantifier : ";

     debugPrintQuant("qcf-proc", q);

     Trace("qcf-proc") << std::endl;

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index f58e89c38..48608cb4e 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -33,6 +33,14 @@ void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, s
     Trace("quant-attr-debug") << "Set conjecture " << n << std::endl;
     ConjectureAttribute ca;
     n.setAttribute( ca, true );
+  }else if( attr=="sygus" ){
+    Trace("quant-attr-debug") << "Set sygus " << n << std::endl;
+    SygusAttribute ca;
+    n.setAttribute( ca, true );
+  }else if( attr=="synthesis" ){
+    Trace("quant-attr-debug") << "Set synthesis " << n << std::endl;
+    SynthesisAttribute ca;
+    n.setAttribute( ca, true );
   }else if( attr=="quant-inst-max-level" ){
     Assert( node_values.size()==1 );
     uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index d142007c6..fb7ff679b 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1117,7 +1117,7 @@ Node QuantifiersRewriter::rewriteRewriteRule( Node r ) {
   NodeBuilder<> patternListB(kind::INST_PATTERN_LIST);
   //the entire rewrite rule is the first pattern
   if( options::quantRewriteRules() ){
-    patternListB << NodeManager::currentNM()->mkNode( INST_PATTERN, r );
+    patternListB << NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, r );
   }
   patternListB << static_cast<Node>(patternB);
   forallB << static_cast<Node>(patternListB);
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 7ec503016..405b3749d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -21,6 +21,8 @@
 #include "theory/quantifiers/theory_quantifiers.h"
 #include "util/datatype.h"
 #include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/quantifiers/rewrite_engine.h"
 
 using namespace std;
 using namespace CVC4;
@@ -991,6 +993,16 @@ void TermDb::computeAttributes( Node q ) {
           Trace("quant-attr") << "Attribute : conjecture : " << q << std::endl;
           d_qattr_conjecture[q] = true;
         }
+        if( avar.getAttribute(SygusAttribute()) ){
+          Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
+          d_qattr_sygus[q] = true;
+          d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+        }
+        if( avar.getAttribute(SynthesisAttribute()) ){
+          Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl;
+          d_qattr_synthesis[q] = true;
+          d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+        }
         if( avar.hasAttribute(QuantInstLevelAttribute()) ){
           d_qattr_qinstLevel[q] = avar.getAttribute(QuantInstLevelAttribute());
           Trace("quant-attr") << "Attribute : quant inst level " << d_qattr_qinstLevel[q] << " : " << q << std::endl;
@@ -999,6 +1011,11 @@ void TermDb::computeAttributes( Node q ) {
           d_qattr_rr_priority[q] = avar.getAttribute(RrPriorityAttribute());
           Trace("quant-attr") << "Attribute : rr priority " << d_qattr_rr_priority[q] << " : " << q << std::endl;
         }
+        if( avar.getKind()==REWRITE_RULE ){
+          Assert( i==0 );
+          //set rewrite engine as owner
+          d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() );
+        }
       }
     }
   }
@@ -1022,6 +1039,24 @@ bool TermDb::isQAttrAxiom( Node q ) {
   }
 }
 
+bool TermDb::isQAttrSygus( Node q ) {
+  std::map< Node, bool >::iterator it = d_qattr_sygus.find( q );
+  if( it==d_qattr_sygus.end() ){
+    return false;
+  }else{
+    return it->second;
+  }
+}
+
+bool TermDb::isQAttrSynthesis( Node q ) {
+  std::map< Node, bool >::iterator it = d_qattr_synthesis.find( q );
+  if( it==d_qattr_synthesis.end() ){
+    return false;
+  }else{
+    return it->second;
+  }
+}
+
 int TermDb::getQAttrQuantInstLevel( Node q ) {
   std::map< Node, int >::iterator it = d_qattr_qinstLevel.find( q );
   if( it==d_qattr_qinstLevel.end() ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e9234bdfe..3bd0563b6 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -33,6 +33,14 @@ typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
 struct ConjectureAttributeId {};
 typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
   
+/** Attribute true for quantifiers that are SyGus conjectures */
+struct SygusAttributeId {};
+typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
+
+/** Attribute true for quantifiers that are synthesis conjectures */
+struct SynthesisAttributeId {};
+typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
+
 /** Attribute true for nodes that should not be used for matching */
 struct NoMatchAttributeId {};
 /** use the special for boolean flag */
@@ -297,6 +305,8 @@ public: //general queries concerning quantified formulas wrt modules
 private:
   std::map< Node, bool > d_qattr_conjecture;
   std::map< Node, bool > d_qattr_axiom;
+  std::map< Node, bool > d_qattr_sygus;
+  std::map< Node, bool > d_qattr_synthesis;
   std::map< Node, int > d_qattr_rr_priority;
   std::map< Node, int > d_qattr_qinstLevel;
   //record attributes
@@ -306,6 +316,10 @@ public:
   bool isQAttrConjecture( Node q );
   /** is axiom */
   bool isQAttrAxiom( Node q );
+  /** is sygus conjecture */
+  bool isQAttrSygus( Node q );
+  /** is synthesis conjecture */
+  bool isQAttrSynthesis( Node q );
   /** get instantiation level */
   int getQAttrQuantInstLevel( Node q );
   /** get rewrite rule priority */