Add --lte-restrict-inst-closure option. Push dt.size fairness constraints inside...

[cvc5.git] / src / theory / quantifiers / theory_quantifiers.cpp

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index b1a7c99270fff2a26820c4410e068c42ca737c08..951a6b54514a901e0bcf9904fed9d674ba87885e 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file theory_quantifiers.cpp
  ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): bobot, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Original author: Morgan Deters
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Dejan Jovanovic
+ ** 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
  **
@@ -33,15 +33,19 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
-  Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, qe),
-  d_numRestarts(0),
+TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+  Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
   d_masterEqualityEngine(0)
 {
   d_numInstantiations = 0;
   d_baseDecLevel = -1;
   out.handleUserAttribute( "axiom", this );
   out.handleUserAttribute( "conjecture", this );
+  out.handleUserAttribute( "fun-def", this );
+  out.handleUserAttribute( "sygus", this );
+  out.handleUserAttribute( "synthesis", this );
+  out.handleUserAttribute( "quant-inst-max-level", this );
+  out.handleUserAttribute( "rr-priority", this );
 }
 
 TheoryQuantifiers::~TheoryQuantifiers() {
@@ -65,7 +69,7 @@ void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) {
 
 void TheoryQuantifiers::preRegisterTerm(TNode n) {
   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
-  if( n.getKind()==FORALL && !n.hasAttribute(InstConstantAttribute()) ){
+  if( n.getKind()==FORALL && !TermDb::hasInstConstAttr(n) ){
     getQuantifiersEngine()->registerQuantifier( n );
   }
 }
@@ -92,27 +96,58 @@ Node TheoryQuantifiers::getValue(TNode n) {
   }
 }
 
-void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){
+void TheoryQuantifiers::computeCareGraph() {
+  //do nothing
+}
 
+void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) {
+  if(fullModel) {
+    for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
+      if((*i).assertion.getKind() == kind::NOT) {
+        Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl;
+        m->assertPredicate((*i).assertion[0], false);
+      } else {
+        Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
+        m->assertPredicate(*i, true);
+      }
+    }
+  }
 }
 
 void TheoryQuantifiers::check(Effort e) {
-  CodeTimer codeTimer(d_theoryTime);
+  if (done() && !fullEffort(e)) {
+    return;
+  }
+
+  TimerStat::CodeTimer checkTimer(d_checkTime);
 
-  Debug("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl;
+  Trace("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl;
   while(!done()) {
     Node assertion = get();
-    Debug("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl;
+    Trace("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl;
     switch(assertion.getKind()) {
     case kind::FORALL:
       assertUniversal( assertion );
       break;
+    case kind::INST_CLOSURE:
+      getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
+      if( !options::lteRestrictInstClosure() ){
+        getQuantifiersEngine()->getMasterEqualityEngine()->addTerm( assertion[0] );
+      }
+      break;
+    case kind::EQUAL:
+      //do nothing
+      break;
     case kind::NOT:
       {
         switch( assertion[0].getKind()) {
         case kind::FORALL:
           assertExistential( assertion );
           break;
+        case kind::EQUAL:
+          //do nothing
+          break;
+        case kind::INST_CLOSURE:
         default:
           Unhandled(assertion[0].getKind());
           break;
@@ -129,7 +164,6 @@ void TheoryQuantifiers::check(Effort e) {
 }
 
 void TheoryQuantifiers::propagate(Effort level){
-  //CodeTimer codeTimer(d_theoryTime);
   //getQuantifiersEngine()->propagate( level );
 }
 
@@ -139,24 +173,15 @@ Node TheoryQuantifiers::getNextDecisionRequest(){
 
 void TheoryQuantifiers::assertUniversal( Node n ){
   Assert( n.getKind()==FORALL );
-  if( !n.hasAttribute(InstConstantAttribute()) ){
-    getQuantifiersEngine()->registerQuantifier( n );
-    getQuantifiersEngine()->assertNode( n );
+  if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){
+    getQuantifiersEngine()->assertQuantifier( n, true );
   }
 }
 
 void TheoryQuantifiers::assertExistential( Node n ){
   Assert( n.getKind()== NOT && n[0].getKind()==FORALL );
-  if( !n[0].hasAttribute(InstConstantAttribute()) ){
-    if( d_skolemized.find( n )==d_skolemized.end() ){
-      Node body = getQuantifiersEngine()->getTermDatabase()->getSkolemizedBody( n[0] );
-      NodeBuilder<> nb(kind::OR);
-      nb << n[0] << body.notNode();
-      Node lem = nb;
-      Debug("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl;
-      d_out->lemma( lem );
-      d_skolemized[n] = true;
-    }
+  if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n[0]) ){
+    getQuantifiersEngine()->assertQuantifier( n[0], false );
   }
 }
 
@@ -173,25 +198,9 @@ bool TheoryQuantifiers::flipDecision(){
   //}else{
   //  return false;
   //}
-
-  if( !d_out->flipDecision() ){
-    return restart();
-  }
-  return true;
-}
-
-bool TheoryQuantifiers::restart(){
-  static const int restartLimit = 0;
-  if( d_numRestarts==restartLimit ){
-    Debug("quantifiers-flip") << "No more restarts." << std::endl;
-    return false;
-  }else{
-    d_numRestarts++;
-    Debug("quantifiers-flip") << "Do restart." << std::endl;
-    return true;
-  }
+  return false;
 }
 
-void TheoryQuantifiers::setUserAttribute( const std::string& attr, Node n ){
-  QuantifiersAttributes::setUserAttribute( attr, n );
+void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
+  QuantifiersAttributes::setUserAttribute( attr, n, node_values, str_value );
 }