Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regressions.

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 8e6673fb972ca35ae66eecfeec263d94f6b03cd5..1f4d398bef8a63f0022a0c35f133bd13ec87a775 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -39,6 +39,7 @@ d_qe( qe ), d_out( out ), d_use_vts_delta( use_vts_delta ), d_use_vts_inf( use_v
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
   d_true = NodeManager::currentNM()->mkConst( true );
+  d_is_nested_quant = false;
 }
 
 void CegInstantiator::computeProgVars( Node n ){
@@ -1202,8 +1203,13 @@ void CegInstantiator::processAssertions() {
       //collect all assertions from theory
       for( context::CDList<Assertion>::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) {
         Node lit = (*it).assertion;
-        d_curr_asserts[tid].push_back( lit );
-        Trace("cbqi-proc-debug") << "...add : " << lit << std::endl;
+        Node atom = lit.getKind()==NOT ? lit[0] : lit;
+        if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){
+          d_curr_asserts[tid].push_back( lit );
+          Trace("cbqi-proc-debug") << "...add : " << lit << std::endl;
+        }else{
+          Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl;
+        }
         if( lit.getKind()==EQUAL ){
           std::map< Node, std::map< Node, Node > >::iterator itae = d_aux_eq.find( lit );
           if( itae!=d_aux_eq.end() ){
@@ -1338,6 +1344,25 @@ void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, st
   subs_rhs.push_back( r );
 }
 
+void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) {
+  if( n.getKind()==FORALL ){
+    d_is_nested_quant = true;
+  }else{
+    if( visited.find( n )==visited.end() ){
+      visited[n] = true;
+      if( TermDb::isBoolConnective( n.getKind() ) ){
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          collectCeAtoms( n[i], visited );
+        }
+      }else{
+        if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){
+          d_ce_atoms.push_back( n );
+        }
+      }
+    }
+  }
+}
+
 void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
   Assert( d_vars.empty() );
   d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
@@ -1367,6 +1392,10 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
     }
     lems[i] = rlem;
   }
+  //collect atoms from lem[0]: we will only do bounds coming from original body
+  d_is_nested_quant = false;
+  std::map< Node, bool > visited;
+  collectCeAtoms( lems[0], visited );
 }
 
 //old implementation

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 9b3b15dc5dda6489aec8ce1d34721152da2caf32..9fe938f167c40db2250e468b8b4de9740f4dc91e 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -65,7 +65,12 @@ private:
   std::map< Node, std::map< Node, Node > > d_aux_eq;
   //the CE variables
   std::vector< Node > d_vars;
+  //atoms of the CE lemma
+  bool d_is_nested_quant;
+  std::vector< Node > d_ce_atoms;
 private:
+  //collect atoms
+  void collectCeAtoms( Node n, std::map< Node, bool >& visited );
   //for adding instantiations during check
   void computeProgVars( Node n );
   //solved form, involves substitution with coefficients

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index b7d82bc9ea77cf8123d675033d929461217d6a34..9e13ef5eb82ae091086ef2e1ecea10f5766c230b 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1649,7 +1649,7 @@ void MatchGen::setInvalid() {
 }
 
 bool MatchGen::isHandledBoolConnective( TNode n ) {
-  return n.getType().isBoolean() && ( n.getKind()==OR || n.getKind()==AND || n.getKind()==IFF || n.getKind()==ITE || n.getKind()==FORALL || n.getKind()==NOT );
+  return n.getType().isBoolean() && TermDb::isBoolConnective( n.getKind() );
 }
 
 bool MatchGen::isHandledUfTerm( TNode n ) {

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 366c7ce072e5386ea1d4014f0b43632e99a4fe1e..2c94308769c21ccbbdd05e0fc977dba9b70b441f 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1549,6 +1549,10 @@ bool TermDb::isComm( Kind k ) {
          k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
 }
 
+bool TermDb::isBoolConnective( Kind k ) {
+  return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT;
+}
+
 void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
   if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
     d_op_triggers[op].push_back( tr );

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 682a9f8e0c06ebf13f48a6edeaf13b37d9eee3f5..1b0b72bf9de94243873a51b25a44e486d4edc04c 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -394,6 +394,8 @@ public:
   static bool isAssoc( Kind k );
   /** is comm */
   static bool isComm( Kind k );
+  /** is bool connective */
+  static bool isBoolConnective( Kind k );
 
 //for sygus
 private:

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f1c47a21a518c8b3edfdd2190b9843530ee2889e..2c2e4ea5b50e2bb3c62edb634bb0e29d393121e4 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -298,7 +298,7 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
 }
 
 void QuantifiersEngine::presolve() {
-  Trace("quant-engine-debug") << "QuantifiersEngine : presolve " << std::endl;
+  Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
   for( unsigned i=0; i<d_modules.size(); i++ ){
     d_modules[i]->presolve();
   }
@@ -306,9 +306,11 @@ void QuantifiersEngine::presolve() {
   d_presolve = false;
   //add all terms to database
   if( options::incrementalSolving() ){
+    Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache.size() << std::endl;
     for( unsigned i=0; i<d_presolve_cache.size(); i++ ){
       addTermToDatabase( d_presolve_cache[i], d_presolve_cache_wq[i], d_presolve_cache_wic[i] );
     }
+    Trace("quant-engine-proc") << "Done add presolve cache " << std::endl;
   }
 }
 
@@ -558,9 +560,9 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
       //generate the phase requirements
       d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
       //also register it with the strong solver
-      if( options::finiteModelFind() ){
-        ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
-      }
+      //if( options::finiteModelFind() ){
+      //  ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
+      //}
       d_quants[f] = true;
       return true;
     }

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 073399894915621cc94eea9fcb8e0ff2bde54d1a..8587610787663939ab9e2ab2b69afdd394c57b0a 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -265,6 +265,9 @@ void TheoryUF::presolve() {
       d_out->lemma(*i);
     }
   }
+  if( d_thss ){
+    d_thss->presolve();
+  }
   Debug("uf") << "uf: end presolve()" << endl;
 }
 

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 2a33b8b362c4ce07c6798c4b6b945dea4d6ff6e4..29e726da73e9cf1c991b56a4b18127df66a06598 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -706,6 +706,11 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
   }
 }
 
+void StrongSolverTheoryUF::SortModel::presolve() {
+  d_initialized = false;
+  d_aloc_cardinality = 0;
+}
+
 void StrongSolverTheoryUF::SortModel::propagate( Theory::Effort level, OutputChannel* out ){
 
 }
@@ -719,11 +724,14 @@ Node StrongSolverTheoryUF::SortModel::getNextDecisionRequest(){
       if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){
         Trace("uf-ss-dec") << "UFSS : Get next decision " << d_type << " " << i << std::endl;
         return cn;
+      }else{
+        Trace("uf-ss-dec-debug") << "  dec : " << cn << " already asserted " << d_cardinality_assertions[cn].get() << std::endl;
       }
     }
   }
   Trace("uf-ss-dec") << "UFSS : no decisions for " << d_type << "." << std::endl;
   Trace("uf-ss-dec-debug") << "  aloc_cardinality = " << d_aloc_cardinality << ", cardinality = " << d_cardinality << ", hasCard = " << d_hasCard << std::endl;
+  Assert( d_hasCard );
   return Node::null();
 }
 
@@ -834,6 +842,7 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int
   if( !d_conflict ){
     Trace("uf-ss-assert") << "Assert cardinality " << d_type << " " << c << " " << val << " level = ";
     Trace("uf-ss-assert") << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl;
+    Assert( c>0 );
     Node cl = getCardinalityLiteral( c );
     d_cardinality_assertions[ cl ] = val;
     if( val ){
@@ -878,10 +887,12 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int
       if( !d_hasCard ){
         bool needsCard = true;
         for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it!=d_cardinality_literal.end(); ++it ){
-          if( d_cardinality_assertions.find( it->second )==d_cardinality_assertions.end() ){
-            Debug("fmf-card-debug") << "..does not need allocate because of " << it->second << std::endl;
-            needsCard = false;
-            break;
+          if( it->first<=d_aloc_cardinality.get() ){
+            if( d_cardinality_assertions.find( it->second )==d_cardinality_assertions.end() ){
+              Debug("fmf-card-debug") << "..does not need allocate because of " << it->second << std::endl;
+              needsCard = false;
+              break;
+            }
           }
         }
         if( needsCard ){
@@ -1702,6 +1713,14 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){
   }
 }
 
+void StrongSolverTheoryUF::presolve() {
+  d_aloc_com_card.set( 0 );
+  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+    it->second->presolve();
+    it->second->initialize( d_out );
+  }
+}
+
 /** propagate */
 void StrongSolverTheoryUF::propagate( Theory::Effort level ){
   //for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
@@ -1779,14 +1798,14 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
   }
 }
 
-void StrongSolverTheoryUF::registerQuantifier( Node f ){
-  Debug("uf-ss-register") << "Register quantifier " << f << std::endl;
+//void StrongSolverTheoryUF::registerQuantifier( Node f ){
+//  Debug("uf-ss-register") << "Register quantifier " << f << std::endl;
   //must ensure the quantifier does not quantify over arithmetic
   //for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
   //  TypeNode tn = f[0][i].getType();
   //  preRegisterType( tn, true );
   //}
-}
+//}
 
 
 StrongSolverTheoryUF::SortModel* StrongSolverTheoryUF::getSortModel( Node n ){
@@ -1798,15 +1817,10 @@ StrongSolverTheoryUF::SortModel* StrongSolverTheoryUF::getSortModel( Node n ){
     it = d_rep_model.find( tn );
   }
   if( it!=d_rep_model.end() ){
-    //initialize the type if necessary
-    //if( d_rep_model_init.find( tn )==d_rep_model_init.end() ){
-      ////initialize the model
-      //it->second->initialize( d_out );
-      //d_rep_model_init[tn] = true;
-    //}
     return it->second;
+  }else{
+    return NULL;
   }
-  return NULL;
 }
 
 void StrongSolverTheoryUF::notifyRestart(){

diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 3619a8ba733ace36ea4f59a593e344ac28eaf6a3..3e612ff1f6d6f7d663bcdac5f3eeb872948b2fe7 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -268,6 +268,8 @@ public:
     bool areDisequal( Node a, Node b );
     /** check */
     void check( Theory::Effort level, OutputChannel* out );
+    /** presolve */
+    void presolve();
     /** propagate */
     void propagate( Theory::Effort level, OutputChannel* out );
     /** get next decision request */
@@ -365,6 +367,8 @@ public:
 public:
   /** check */
   void check( Theory::Effort level );
+  /** presolve */
+  void presolve();
   /** propagate */
   void propagate( Theory::Effort level );
   /** get next decision request */
@@ -372,7 +376,7 @@ public:
   /** preregister a term */
   void preRegisterTerm( TNode n );
   /** preregister a quantifier */
-  void registerQuantifier( Node f );
+  //void registerQuantifier( Node f );
   /** notify restart */
   void notifyRestart();
 public:

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

diff --git a/test/regress/regress0/push-pop/fmf-fun-dbu.smt2 b/test/regress/regress0/push-pop/fmf-fun-dbu.smt2
new file mode 100644 (file)
index 0000000..125d5fc
--- /dev/null
+++ b/test/regress/regress0/push-pop/fmf-fun-dbu.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --incremental --fmf-fun --no-check-models
+(set-logic UFDTLIA)
+(set-option :produce-models true)
+(set-info :smt-lib-version 2.5)
+(declare-datatypes () ((List (Nil) (Cons (Cons$head Int) (Cons$tail List)))))
+(define-fun-rec all-z ((x List)) Bool (=> (is-Cons x) (and (= 0 (Cons$head x)) (all-z (Cons$tail x)))))
+(define-fun-rec len ((x List)) Int (ite (is-Nil x) 0 (+ 1 (len (Cons$tail x)))))
+(declare-fun root() List)
+; EXPECT: sat
+(assert (and (all-z root) (<= 1 (len root))))
+(check-sat)
+; EXPECT: sat
+(assert (= root (Cons 0 Nil)))
+(check-sat)
+

diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 6bd732c766443c1dcb1e3507c165e555de074c82..a1f91a6cefa15ec8f25e21dcb6f1ccf4c092fbaf 100644 (file)
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -44,7 +44,8 @@ TESTS = commutative.sy \
         uminus_one.sy \
         sygus-dt.sy \
         dt-no-syntax.sy \
-        list-head-x.sy
+        list-head-x.sy \
+        clock-inc-tuple.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \

diff --git a/test/regress/regress0/sygus/clock-inc-tuple.sy b/test/regress/regress0/sygus/clock-inc-tuple.sy
new file mode 100644 (file)
index 0000000..09bdb8b
--- /dev/null
+++ b/test/regress/regress0/sygus/clock-inc-tuple.sy
@@ -0,0 +1,14 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si --no-dump-synth
+
+(set-logic ALL_SUPPORTED)
+(declare-var m Int)
+(declare-var s Int)
+(declare-var inc Int)
+(declare-datatypes () ( (tuple2 (tuple2 (_m Int) (_s Int))) ))
+
+(synth-fun x12 ((m Int) (s Int) (inc Int)) tuple2)
+(constraint (=> 
+(and (>= m 0) (>= s 0) (< s 3) (> inc 0)) 
+(and (>= (_m (x12 m s inc)) 0) (>= (_s (x12 m s inc)) 0) (< (_s (x12 m s inc)) 3) (= (+ (* (_m (x12 m s inc)) 3) (_s (x12 m s inc))) (+ (+ (* m 3) s) inc)))))
+(check-synth)