Bug fix for define functions + incremental. Minor work on relational triggers.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5e97158cae2a3e23a0ad36ec9f0f55f371a9b6c7..bbaa07af5d2c607e6fe3c36d357973668333f295 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2123,6 +2123,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
 void SmtEngine::defineFunction(Expr func,
                                const std::vector<Expr>& formals,
                                Expr formula) {
+  SmtScope smts(this);
+  doPendingPops();
   Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
   for(std::vector<Expr>::const_iterator i = formals.begin(); i != formals.end(); ++i) {
     if((*i).getKind() != kind::BOUND_VARIABLE) {
@@ -2141,7 +2143,6 @@ void SmtEngine::defineFunction(Expr func,
   DefineFunctionCommand c(ss.str(), func, formals, formula);
   addToModelCommandAndDump(c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
 
-  SmtScope smts(this);
 
   PROOF( if (options::checkUnsatCores()) {
       d_defineCommands.push_back(c.clone());

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 680be77daa27f6459c102b4f8b3d7480d2a9d7ee..1f68884b6602fd33cd7691164e2b49c89b9fa8fc 100644 (file)
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -130,21 +130,37 @@ Node CandidateGeneratorQE::getNextCandidate(){
 
 CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) :
   d_match_pattern( mpat ), d_qe( qe ){
-
+  Assert( mpat.getKind()==EQUAL );
+  for( unsigned i=0; i<2; i++ ){
+    if( !quantifiers::TermDb::hasInstConstAttr(mpat[i]) ){
+      d_match_gterm = mpat[i];
+    }
+  }
 }
 void CandidateGeneratorQELitEq::resetInstantiationRound(){
 
 }
 void CandidateGeneratorQELitEq::reset( Node eqc ){
-  d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+  if( d_match_gterm.isNull() ){
+    d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+  }else{
+    d_do_mgt = true;
+  }
 }
 Node CandidateGeneratorQELitEq::getNextCandidate(){
-  while( !d_eq.isFinished() ){
-    Node n = (*d_eq);
-    ++d_eq;
-    if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){
-      //an equivalence class with the same type as the pattern, return reflexive equality
-      return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
+  if( d_match_gterm.isNull() ){
+    while( !d_eq.isFinished() ){
+      Node n = (*d_eq);
+      ++d_eq;
+      if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){
+        //an equivalence class with the same type as the pattern, return reflexive equality
+        return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
+      }
+    }
+  }else{
+    if( d_do_mgt ){
+      d_do_mgt = false;
+      return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_gterm, d_match_gterm );
     }
   }
   return Node::null();

diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index fb120dd080fdd6313e3a9a9c703ede7dd878877a..d86891de72359bb47da966e3728cb33aa1d98fb6 100644 (file)
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -108,6 +108,8 @@ private:
   eq::EqClassesIterator d_eq;
   //equality you are trying to match equalities for
   Node d_match_pattern;
+  Node d_match_gterm;
+  bool d_do_mgt;
   //einstantiator pointer
   QuantifiersEngine* d_qe;
 public:

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 621327c0b8ca13f36cea458b590b06842bd6d746..111eab1165c54d70ff89548467c7be4099bfa757 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -51,10 +51,12 @@ struct sortQuantifiersForSymbol {
 
 struct sortTriggers {
   bool operator() (Node i, Node j) {
-    if( Trigger::isAtomicTrigger( i ) ){
-      return i<j || !Trigger::isAtomicTrigger( j );
+    int wi = Trigger::getTriggerWeight( i );
+    int wj = Trigger::getTriggerWeight( j );
+    if( wi==wj ){
+      return i<j;
     }else{
-      return i<j && !Trigger::isAtomicTrigger( j );
+      return wi<wj;
     }
   }
 };
@@ -257,19 +259,20 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
       Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true );
       Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
-      for( int i=0; i<(int)patTermsF.size(); i++ ){
-        Trace("auto-gen-trigger-debug") << "   " << patTermsF[i] << std::endl;
-      }
-      Trace("auto-gen-trigger-debug") << std::endl;
       if( ntrivTriggers ){
         sortTriggers st;
         std::sort( patTermsF.begin(), patTermsF.end(), st );
       }
+      for( unsigned i=0; i<patTermsF.size(); i++ ){
+        Trace("auto-gen-trigger-debug") << "   " << patTermsF[i] << std::endl;
+      }
+      Trace("auto-gen-trigger-debug") << std::endl;
     }
     //sort into single/multi triggers
     std::map< Node, std::vector< Node > > varContains;
     std::map< Node, bool > vcMap;
     std::map< Node, bool > rmPatTermsF;
+    int last_weight = -1;
     for( unsigned i=0; i<patTermsF.size(); i++ ){
       d_quantEngine->getTermDatabase()->getVarContainsNode( f, patTermsF[i], varContains[ patTermsF[i] ] );
       bool newVar = false;
@@ -279,9 +282,12 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
           newVar = true;
         }
       }
-      if( ntrivTriggers && !newVar && !Trigger::isAtomicTrigger( patTermsF[i] ) ){
+      int curr_w = Trigger::getTriggerWeight( patTermsF[i] );
+      if( ntrivTriggers && !newVar && last_weight!=-1 && curr_w>last_weight ){
         Trace("auto-gen-trigger-debug") << "Exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl;
         rmPatTermsF[patTermsF[i]] = true;
+      }else{
+        last_weight = curr_w;
       }
     }
     for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 0628b7fbc7e65d9d189327371d956ab330318ba3..48385e28b8d137d9bdf3473f9ef101a1b88d3206 100644 (file)
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -242,7 +242,7 @@ bool Trigger::isUsable( Node n, Node q ){
 }
 
 Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
-  Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
+  Trace("trigger-debug") << "Is " << n << " a usable trigger? pol/hasPol=" << pol << "/" << hasPol << std::endl;
   if( n.getKind()==NOT ){
     pol = !pol;
     n = n[0];
@@ -254,7 +254,8 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
       bool is_arith = n[0].getType().isReal();
       for( unsigned i=0; i<2; i++) {
         if( n[1-i].getKind()==INST_CONSTANT ){
-          if( isUsableTrigger( n[i], f ) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) && ( !do_negate || is_arith ) ){
+          if( ( ( isUsableTrigger( n[i], f ) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) ) || !quantifiers::TermDb::hasInstConstAttr(n[i]) ) && 
+              ( !do_negate || is_arith ) ){
             rtr = n;
             break;
           }
@@ -274,7 +275,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
               Node veq;
               if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){
                 int vti = veq[0]==it->first ? 1 : 0;
-                if( isUsableTrigger( veq[vti], f ) && !quantifiers::TermDb::containsTerm( veq[vti], veq[1-vti] ) ){
+                if( ( isUsableTrigger( veq[vti], f ) && !quantifiers::TermDb::containsTerm( veq[vti], veq[1-vti] ) ) || !quantifiers::TermDb::hasInstConstAttr(veq[vti]) ){
                   rtr = veq;
                 }
               }
@@ -434,6 +435,23 @@ bool Trigger::isPureTheoryTrigger( Node n ) {
   }
 }
 
+int Trigger::getTriggerWeight( Node n ) {
+  if( isAtomicTrigger( n ) ){
+    return 0;
+  }else{
+    if( options::relationalTriggers() ){
+      if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
+        for( unsigned i=0; i<2; i++ ){
+          if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermDb::hasInstConstAttr( n[1-i] ) ){
+            return 0;
+          }
+        }
+      }
+    }
+    return 1;
+  }
+}
+
 bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) {
   if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
     if( std::find( patTerms.begin(), patTerms.end(), n )==patTerms.end() ){

diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 11962008e9f8b2da413a065fa79dc02aebb2d8bf..bbbf9495f7d7941053574a40881f827836c39319 100644 (file)
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -112,6 +112,7 @@ public:
   static bool isSimpleTrigger( Node n );
   static bool isBooleanTermTrigger( Node n );
   static bool isPureTheoryTrigger( Node n );
+  static int getTriggerWeight( Node n );
   static bool isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms );
   /** return data structure for producing matches for this trigger. */
   static InstMatchGenerator* getInstMatchGenerator( Node q, Node n );

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 4be55ebb5803383e585e35b531a23b3a8c819c6e..754b0c22432aa7af8428a31b48a68c3e88f0460b 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -88,6 +88,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
     d_te( te ),
     d_lemmas_produced_c(u),
     d_skolemized(u),
+    d_ierCounter_c(c),
     //d_ierCounter(c),
     //d_ierCounter_lc(c),
     //d_ierCounterLastLc(c),
@@ -143,6 +144,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   d_total_inst_count_debug = 0;
   //allow theory combination to go first, once initially
   d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
+  d_ierCounter_c = d_ierCounter;
   d_ierCounter_lc = 0;
   d_ierCounterLastLc = 0;
   d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
@@ -375,6 +377,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
   if( needsCheck ){
     if( Trace.isOn("quant-engine-debug") ){
       Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
+      Trace("quant-engine-debug") << "  depth : " << d_ierCounter_c << std::endl;
       Trace("quant-engine-debug") << "  modules to check : ";
       for( unsigned i=0; i<qm.size(); i++ ){
         Trace("quant-engine-debug") << qm[i]->identify() << " ";
@@ -470,6 +473,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
             if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){
               d_ierCounter = d_ierCounter + 1;
               d_ierCounterLastLc = d_ierCounter_lc;
+              d_ierCounter_c = d_ierCounter_c.get() + 1;
             }
           }else if( e==Theory::EFFORT_LAST_CALL ){
             d_ierCounter_lc = d_ierCounter_lc + 1;

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 228ac9ee9ace0d6a6621cbcef99c7ecfb40ab1df..920c45c1a1f882780211b3dd0ba284a0a19d0953 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -204,6 +204,7 @@ private:
   std::map< Node, int > d_temp_inst_debug;
   int d_total_inst_count_debug;
   /** inst round counters TODO: make context-dependent? */
+  context::CDO< int > d_ierCounter_c;
   int d_ierCounter;
   int d_ierCounter_lc;
   int d_ierCounterLastLc;

diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index bcf6403b7a837a805dc6d0782e603bd3be978785..4bc16ea25bf66ae72504a3b9c576ab12d676b088 100644 (file)
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -44,7 +44,8 @@ BUG_TESTS = \
   bug-fmf-fun-skolem.smt2 \
   bug674.smt2 \
   inc-double-u.smt2 \
-  fmf-fun-dbu.smt2
+  fmf-fun-dbu.smt2 \
+  inc-define.smt2
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 

diff --git a/test/regress/regress0/push-pop/inc-define.smt2 b/test/regress/regress0/push-pop/inc-define.smt2
new file mode 100644 (file)
index 0000000..27261ef
--- /dev/null
+++ b/test/regress/regress0/push-pop/inc-define.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(check-sat)
+(define t (not (= x 0)))
+(assert t)
+(check-sat)