Avoid ensureLiteral on unpreprocessed formulas in cbqi.

diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015
index 831c892bed6e31c42a081e8c5eb158cb654c7625..c66ee11c63f71739d003d507d8a5fbd7da73d346 100644 (file)
--- a/contrib/run-script-smtcomp2015
+++ b/contrib/run-script-smtcomp2015
@@ -67,12 +67,11 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
   finishwith --full-saturate-quant
   ;;
 LIA|LRA|NIA|NRA)
-  trywith 20 --enable-cbqi --full-saturate-quant
+  trywith 20 --cbqi --full-saturate-quant
   trywith 20 --full-saturate-quant
-  trywith 20 --cbqi-recurse --full-saturate-quant
-  trywith 30 --quant-cf --full-saturate-quant
-  trywith 60 --quant-cf --qcf-tconstraint --full-saturate-quant
-  trywith 120 --cbqi-recurse --disable-prenex-quant --full-saturate-quant
+  trywith 20 --cbqi --cbqi-recurse --full-saturate-quant
+  trywith 60 --qcf-tconstraint --full-saturate-quant
+  trywith 120 --cbqi --cbqi-recurse --full-saturate-quant
   finishwith --cbqi-recurse --pre-skolem-quant --full-saturate-quant
   ;;
 QF_AUFBV)

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 12d6bed8d21e80a90079f858b09e49fe5762318d..f530f7b9d898a9f62f8da0fb707c1155ca9a3fea 100644 (file)
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -95,21 +95,20 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
       Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
       if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){
         d_added_cbqi_lemma[f] = true;
-        Debug("cbqi") << "Do cbqi for " << f << std::endl;
+        Trace("cbqi") << "Do cbqi for " << f << std::endl;
         //add cbqi lemma
         //get the counterexample literal
         Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f );
-        if( !ceLit.isNull() ){
+        Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
+        if( !ceBody.isNull() ){
+          //add counterexample lemma
+          Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
           //require any decision on cel to be phase=true
-          //d_quantEngine->getOutputChannel().requirePhase( ceLit, true );
           d_quantEngine->addRequirePhase( ceLit, true );
           Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
           //add counterexample lemma
-          NodeBuilder<> nb(kind::OR);
-          nb << f << ceLit;
-          Node lem = nb;
+          lem = Rewriter::rewrite( lem );
           Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
-          //d_quantEngine->getOutputChannel().lemma( lem, false, true );
           d_quantEngine->addLemma( lem, false );
           addedLemma = true;
         }
@@ -125,7 +124,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
     InstStrategy* is = d_instStrategies[i];
     is->processResetInstantiationRound( effort );
   }
-  
+
   //iterate over an internal effort level e
   int e = 0;
   int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 62eb786797661bb8a1930a32c79b529f5df209f6..1082bed234c26bb62f4c34fa0e1ea43d7590f2e0 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -741,6 +741,7 @@ Node TermDb::getInstConstantBody( Node f ){
 
 Node TermDb::getCounterexampleLiteral( Node f ){
   if( d_ce_lit.find( f )==d_ce_lit.end() ){
+    /*
     Node ceBody = getInstConstantBody( f );
     //check if any variable are of bad types, and fail if so
     for( size_t i=0; i<d_inst_constants[f].size(); i++ ){
@@ -749,8 +750,10 @@ Node TermDb::getCounterexampleLiteral( Node f ){
         return Node::null();
       }
     }
+    */
+    Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
     //otherwise, ensure literal
-    Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() );
+    Node ceLit = d_quantEngine->getValuation().ensureLiteral( g );
     d_ce_lit[ f ] = ceLit;
   }
   return d_ce_lit[ f ];
@@ -1191,7 +1194,7 @@ bool TermDb::isFunDef( Node q ) {
 }
 
 Node TermDb::getFunDefHead( Node q ) {
-  //&& ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && 
+  //&& ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF &&
   if( q.getKind()==FORALL && q.getNumChildren()==3 ){
     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
       if( q[2][i].getKind()==INST_ATTRIBUTE ){
@@ -1972,7 +1975,7 @@ TypeNode TermDbSygus::getArgType( const DatatypeConstructor& c, int i ) {
 }
 
 Node TermDbSygus::minimizeBuiltinTerm( Node n ) {
-  if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) && 
+  if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) &&
       ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){
     bool changed = false;
     std::vector< Node > mon[2];

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c940b321856dd2dce6b6c0bb7180f7e293c5cd48..afc607470c82ad3200661e8de6617e9b54cff9ac 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -45,7 +45,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
 unsigned QuantifiersModule::needsModel( Theory::Effort e ) {
-  return QuantifiersEngine::QEFFORT_NONE;  
+  return QuantifiersEngine::QEFFORT_NONE;
 }
 
 eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 6468d4650d0d6f0230d07405f2e56963fd550fe0..e613ef2845a7388e281f2834fc20e70b1e4f21a3 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -266,8 +266,6 @@ public:
   Node getInstantiation( Node f, std::vector< Node >& terms );
   /** do substitution */
   Node getSubstitute( Node n, std::vector< Node >& terms );
-  /** exist instantiation ? */
-  //bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
   /** add lemma lem */
   bool addLemma( Node lem, bool doCache = true );
   /** add require phase */

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d0a1eb696f3c52d6f3afa98d8356784a07bb81cf..bbeec5125db1df8f2c72fa7a3e3f05beefaf02de 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -428,7 +428,8 @@ void TheoryEngine::check(Theory::Effort effort) {
       }
     }
 
-    Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas") << endl;
+    Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas");
+    Debug("theory") << ", need check = " << needCheck() << endl;
 
     if(!d_inConflict && Theory::fullEffort(effort) && d_masterEqualityEngine != NULL && !d_lemmasAdded) {
       AlwaysAssert(d_masterEqualityEngine->consistent());