diff options
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 36 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.h | 2 | ||||
| -rw-r--r-- | test/regress/regress0/push-pop/Makefile.am | 3 | ||||
| -rwxr-xr-x | test/regress/regress0/push-pop/bug654-dd.smt2 | 27 |
4 files changed, 55 insertions, 13 deletions
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index d913cb76a..2a33b8b36 100644 --- 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 af316927d..3619a8ba7 100644 --- 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 59531ce8a..bcd8da228 100644 --- 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 index 000000000..01c81cdc8 --- /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 |