diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-05 12:02:28 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-05 12:11:02 +0200 |
commit | c38245e4f041252df011a024abe834ae7ec0ec0a (patch) | |
tree | 0452b7a998312393a2556c6cdf695af17efb91d4 | |
parent | d3c365a60c88e33a7d73f81484db2cff5ef69bbb (diff) |
Fix bugs related to fmf with incremental. Reinitialize sorts on user pop, bug fix enumeration for uninitialized sorts, do not decide combined cardinality constraints that have not been allocated in user context. Fixes bug 654.
-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 |