Fix bugs related to fmf with incremental. Reinitialize sorts on user pop, bug fix...

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index d913cb76a10fcd856aa13446d893259efca5f436..2a33b8b362c4ce07c6798c4b6b945dea4d6ff6e4 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -405,7 +405,7 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in
 StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ),
           d_thss( thss ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ),
           d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( u, 0 ),
-          d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ){
+          d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ){
   d_cardinality_term = n;
   //if( d_type.isSort() ){
   //  TypeEnumerator te(tn);
@@ -417,7 +417,10 @@ StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context
 
 /** initialize */
 void StrongSolverTheoryUF::SortModel::initialize( OutputChannel* out ){
-  allocateCardinality( out );
+  if( !d_initialized ){
+    d_initialized = true;
+    allocateCardinality( out );
+  }
 }
 
 /** new node */
@@ -714,11 +717,13 @@ Node StrongSolverTheoryUF::SortModel::getNextDecisionRequest(){
       Node cn = d_cardinality_literal[ i ];
       Assert( !cn.isNull() );
       if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){
-        Trace("uf-ss-dec") << "Propagate as decision " << d_type << " " << i << std::endl;
+        Trace("uf-ss-dec") << "UFSS : Get next decision " << d_type << " " << i << std::endl;
         return cn;
       }
     }
   }
+  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;
   return Node::null();
 }
 
@@ -1444,7 +1449,7 @@ bool StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){
         Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "enumeration to meet negative card constraint" );
         d_fresh_aloc_reps.push_back( nn );
       }
-      if( d_maxNegCard==1 ){
+      if( d_maxNegCard==0 ){
         m->d_rep_set.d_type_reps[d_type].push_back( d_fresh_aloc_reps[0] );
       }else{
         //must add lemma
@@ -1711,12 +1716,16 @@ Node StrongSolverTheoryUF::getNextDecisionRequest(){
     int comCard = 0;
     Node com_lit;
     do {
-      com_lit = d_com_card_literal.find( comCard )!=d_com_card_literal.end() ? d_com_card_literal[comCard] : Node::null();
-      if( !com_lit.isNull() && d_com_card_assertions.find( com_lit )==d_com_card_assertions.end() ){
-        Trace("uf-ss-dec") << "Decide on combined cardinality : " << com_lit << std::endl;
-        return com_lit;
+      if( comCard<d_aloc_com_card.get() ){
+        com_lit = d_com_card_literal.find( comCard )!=d_com_card_literal.end() ? d_com_card_literal[comCard] : Node::null();
+        if( !com_lit.isNull() && d_com_card_assertions.find( com_lit )==d_com_card_assertions.end() ){
+          Trace("uf-ss-dec") << "Decide on combined cardinality : " << com_lit << std::endl;
+          return com_lit;
+        }
+        comCard++;
+      }else{
+        com_lit = Node::null();
       }
-      comCard++;
     }while( !com_lit.isNull() );
   }
   //otherwise, check each individual sort
@@ -1726,6 +1735,7 @@ Node StrongSolverTheoryUF::getNextDecisionRequest(){
       return n;
     }
   }
+  Trace("uf-ss-dec") << "...no UF SS decisions." << std::endl;
   return Node::null();
 }
 
@@ -1736,10 +1746,11 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
   Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
   //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
   TypeNode tn = n.getType();
-  if( d_rep_model.find( tn )==d_rep_model.end() ){
+  std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
+  if( it==d_rep_model.end() ){
     SortModel* rm = NULL;
     if( tn.isSort() ){
-      Trace("uf-ss-register") << "Preregister sort " << tn << "." << std::endl;
+      Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl;
       rm  = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this );
       //getOutputChannel().lemma( n.eqNode( rm->getCardinalityTerm() ) );
     }else{
@@ -1763,7 +1774,8 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
       //d_rep_model_init[tn] = true;
     }
   }else{
-    Trace("uf-ss-register") << "Already preregistered sort " << tn << "." << std::endl;
+    //ensure sort model is initialized
+    it->second->initialize( d_out );
   }
 }
 

diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index af316927dcf2f699be5512ccd10ee587c845aaf1..3619a8ba733ace36ea4f59a593e344ac28eaf6a3 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -244,6 +244,8 @@ public:
     context::CDO< int > d_maxNegCard;
     /** list of fresh representatives allocated */
     std::vector< Node > d_fresh_aloc_reps;
+    /** whether we are initialized */
+    context::CDO< bool > d_initialized;
   private:
     /** apply totality */
     bool applyTotality( int cardinality );

diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 59531ce8a3fa1d4c9c690d3efee006168cbf1174..bcd8da228acca290e047138a2dc6c1624683ecdc 100644 (file)
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -39,7 +39,8 @@ BUG_TESTS = \
   arith_lra_02.smt2 \
   quant-fun-proc.smt2 \
   quant-fun-proc-unmacro.smt2 \
-  quant-fun-proc-unfd.smt2 
+  quant-fun-proc-unfd.smt2 \
+  bug654-dd.smt2
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 

diff --git a/test/regress/regress0/push-pop/bug654-dd.smt2 b/test/regress/regress0/push-pop/bug654-dd.smt2
new file mode 100755 (executable)
index 0000000..01c81cd
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug654-dd.smt2
@@ -0,0 +1,27 @@
+; COMMAND-LINE: --incremental --fmf-fun --strings-exp
+(set-logic ALL_SUPPORTED)
+(declare-datatypes () (
+(List_T_C (List_T_C$CNil_T_CustomerType) (ListTC (ListTC$head T_CustomerType) (ListTC$tail List_T_C)))
+(T_CustomerType (T_CustomerType$C_T_CustomerType (T_CustomerType$C_T_CustomerType$a_CompanyName Int) (T_CustomerType$C_T_CustomerType$a_ContactName Int) (ID Int)))
+))
+(declare-fun f (List_T_C) Bool)
+(declare-fun tail_uf_1 (List_T_C) List_T_C)
+(declare-fun head_uf_2 (List_T_C) T_CustomerType)
+(declare-sort U 0)
+(declare-fun a (U) List_T_C)
+(declare-fun z (U) U)
+(assert 
+(forall ((?i U)) 
+(= (f (a ?i)) (not (is-ListTC (a ?i))) 
+)))
+(assert 
+(forall ((?i U)) 
+(= (a (z ?i)) (tail_uf_1 (a ?i)))) ) 
+; EXPECT: sat
+(push 1)
+(check-sat)
+(pop 1)
+; EXPECT: sat
+(push 1)
+(check-sat)
+(pop 1)
\ No newline at end of file