Fix bug in --term-db-mode=relevant with variable triggers. Support inst-closure predicate and mode --term-db-inst-closure. Minor changes to theory_quantifiers.

1 files changed, 15 insertions, 18 deletions

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 5c68e52a7..de0f98af6 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -35,7 +35,6 @@ using namespace CVC4::theory::quantifiers;
 
 TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
   Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
-  d_numRestarts(0),
   d_masterEqualityEngine(0)
 {
   d_numInstantiations = 0;
@@ -97,6 +96,10 @@ Node TheoryQuantifiers::getValue(TNode n) {
   }
 }
 
+void TheoryQuantifiers::computeCareGraph() {
+  //do nothing
+}
+
 void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) {
   if(fullModel) {
     for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
@@ -126,12 +129,22 @@ void TheoryQuantifiers::check(Effort e) {
     case kind::FORALL:
       assertUniversal( assertion );
       break;
+    case kind::INST_CLOSURE:
+      getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
+      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: //cannot negate inst closure
         default:
           Unhandled(assertion[0].getKind());
           break;
@@ -182,23 +195,7 @@ 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, std::vector<Node> node_values, std::string str_value){