From 36a5437abbddd484b8bdb18c024cc7573240054f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 5 Nov 2014 15:32:48 +0100 Subject: [PATCH] More work on datatypes theory combination: fix bug in care graph, do not assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind. Minor fixes for fun_def_process. Other minor changes. --- src/theory/datatypes/theory_datatypes.cpp | 80 ++++++++++++++++--- src/theory/quantifiers/fun_def_process.cpp | 11 ++- src/theory/quantifiers/trigger.cpp | 29 +++++++ src/theory/quantifiers/trigger.h | 3 + src/theory/uf/theory_uf_type_rules.h | 4 +- test/regress/regress0/fmf/Makefile.am | 1 + .../regress0/fmf/lst-no-self-rev-exp.smt2 | 31 +++++++ 7 files changed, 140 insertions(+), 19 deletions(-) create mode 100644 test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index c03040868..83d14149b 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -60,7 +60,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine.addFunctionKind(kind::DT_SIZE); d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); - d_equalityEngine.addFunctionKind(kind::APPLY_UF); + //d_equalityEngine.addFunctionKind(kind::APPLY_UF); d_true = NodeManager::currentNM()->mkConst( true ); d_dtfCounter = 0; @@ -1073,6 +1073,36 @@ EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){ void TheoryDatatypes::computeCareGraph(){ Trace("dt-cg") << "Compute graph for dt..." << std::endl; + /* + Trace("dt-cg") << "Look at shared terms..." << std::endl; + for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) { + TNode a = d_sharedTerms[i]; + if( a.getKind()!=APPLY_CONSTRUCTOR && a.getKind()!=APPLY_SELECTOR_TOTAL ){ + TypeNode aType = a.getType(); + for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) { + TNode b = d_sharedTerms[j]; + if( b.getKind()!=APPLY_CONSTRUCTOR && b.getKind()!=APPLY_SELECTOR_TOTAL ){ + if (b.getType() != aType) { + // We don't care about the terms of different types + continue; + } + switch (d_valuation.getEqualityStatus(a, b)) { + case EQUALITY_TRUE_AND_PROPAGATED: + case EQUALITY_FALSE_AND_PROPAGATED: + // If we know about it, we should have propagated it, so we can skip + break; + default: + // Let's split on it + addCarePair(a, b); + break; + } + } + } + } + } + */ + + Trace("dt-cg") << "Look at theory terms..." << std::endl; vector< pair > currentPairs; for( unsigned r=0; r<2; r++ ){ unsigned functionTerms = r==0 ? d_consTerms.size() : d_selTerms.size(); @@ -1096,7 +1126,7 @@ void TheoryDatatypes::computeCareGraph(){ Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl; if( d_equalityEngine.isTriggerTerm(x, THEORY_DATATYPES) && d_equalityEngine.isTriggerTerm(y, THEORY_DATATYPES) ){ EqualityStatus eqStatus = d_valuation.getEqualityStatus(x, y); - if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_UNKNOWN ){ + if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){ somePairIsDisequal = true; break; }else{ @@ -1174,11 +1204,26 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ //for all equivalence classes that are datatypes if( DatatypesRewriter::isTermDatatype( eqc ) ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); - if( !ei->d_constructor.get().isNull() ){ - cons.push_back( ei->d_constructor.get() ); - eqc_cons[ eqc ] = ei->d_constructor.get(); + if( ei && !ei->d_constructor.get().isNull() ){ + Node c = ei->d_constructor.get(); + cons.push_back( c ); + eqc_cons[ eqc ] = c; }else{ - nodes.push_back( eqc ); + //if eqc contains a symbol known to datatypes (a selector), then we must assign + bool containsTSym = false; + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + Trace("dt-cmi-debug") << n << " has kind " << n.getKind() << ", isVar = " << n.isVar() << std::endl; + if( n.isVar() || n.getKind()==APPLY_SELECTOR_TOTAL ){ + containsTSym = true; + break; + } + ++eqc_i; + } + if( containsTSym ){ + nodes.push_back( eqc ); + } } } ++eqccs_i; @@ -1199,6 +1244,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; TypeNode tn = eqc.getType(); //if it is infinite, make sure it is fresh + // this ensures that the term that this is an argument of is distinct. if( eqc.getType().getCardinality().isInfinite() ){ std::map< TypeNode, int >::iterator it = typ_enum_map.find( tn ); int teIndex; @@ -1753,7 +1799,7 @@ bool TheoryDatatypes::mustSpecifyAssignment(){ } bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ - //the datatypes decision procedure makes 5 "internal" inferences apart from the equality engine : + //the datatypes decision procedure makes "internal" inferences apart from the equality engine : // (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si // (2) Label : ~is_C1( t ) ... ~is_C{i-1}( t ) ~is_C{i+1}( t ) ... ~is_Cn( t ) => is_Ci( t ) // (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) ) @@ -1764,12 +1810,20 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl; bool addLemma = false; if( n.getKind()==EQUAL || n.getKind()==IFF ){ - TypeNode tn = n[0].getType(); - if( !tn.isDatatype() ){ - addLemma = true; - }else{ - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - addLemma = dt.involvesExternalType(); + for( unsigned i=0; i<2; i++ ){ + if( n[i].getKind()!=APPLY_SELECTOR_TOTAL && n[i].getKind()!=APPLY_CONSTRUCTOR ){ + addLemma = true; + } + } + + if( !addLemma ){ + TypeNode tn = n[0].getType(); + if( !DatatypesRewriter::isTypeDatatype( tn ) ){ + addLemma = true; + }else{ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + addLemma = dt.involvesExternalType(); + } } //for( int j=0; j<(int)n[1].getNumChildren(); j++ ){ // if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){ diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 0e365c875..cb772a31f 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -71,9 +71,10 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { } Node bd = assertions[i][1].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << " to "; + Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl; + Trace("fmf-fun-def") << " to " << std::endl; assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ); - Trace("fmf-fun-def") << assertions[i] << std::endl; + Trace("fmf-fun-def") << " " << assertions[i] << std::endl; fd_assertions.push_back( i ); } } @@ -86,7 +87,9 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { Assert( constraints.empty() ); if( n!=assertions[i] ){ n = Rewriter::rewrite( n ); - Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << " to " << n << std::endl; + Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << std::endl; + Trace("fmf-fun-def-rewrite") << " to " << std::endl; + Trace("fmf-fun-def-rewrite") << " " << n << std::endl; assertions[i] = n; } } @@ -139,7 +142,7 @@ Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& co }else{ //must add at higher level } - return c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( AND, c ); + return c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( pol ? AND : OR, c ); } }else{ //simplify term diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index b2b8e7197..511103019 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -385,6 +385,30 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< } } +bool Trigger::isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms ) { + if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){ + bool hasVar = false; + for( unsigned i=0; i& patTerms ) { + std::vector< Node > var_found; + return isLocalTheoryExt2( n, var_found, patTerms ); +} + void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){ std::map< Node, bool > patMap; if( filterInst ){ diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 75ada4f83..482701a82 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -95,6 +95,8 @@ private: static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false ); /** collect all APPLY_UF pattern terms for f in n */ static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ); + /** is local theory extensions term */ + static bool isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms ); public: //different strategies for choosing trigger terms enum { @@ -111,6 +113,7 @@ public: static bool isSimpleTrigger( Node n ); static bool isBooleanTermTrigger( Node n ); static bool isPureTheoryTrigger( Node n ); + static bool isLocalTheoryExt( Node n, std::vector< Node >& patTerms ); /** return data structure for producing matches for this trigger. */ static InstMatchGenerator* getInstMatchGenerator( Node n ); static Node getInversionVariable( Node n ); diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index c30742ac5..93fd1dc6f 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -91,8 +91,8 @@ public: if( n[0].getKind()!=kind::CONST_RATIONAL ){ throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be a constant"); } - if( n[0].getConst().getNumerator().sgn()!=1 ){ - throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be positive"); + if( n[0].getConst().getNumerator().sgn()==-1 ){ + throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be non-negative"); } } return nodeManager->booleanType(); diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index e3bfd39b8..cb58ea007 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -40,6 +40,7 @@ EXTRA_DIST = $(TESTS) # disabled for now : # bug0909.smt2 +# lst-no-self-rev-exp.smt2 #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 new file mode 100644 index 000000000..e86d8c60e --- /dev/null +++ b/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 @@ -0,0 +1,31 @@ +; COMMAND-LINE: --finite-model-find --uf-ss-fair +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-datatypes () ((Nat (succ (pred Nat)) (zero)) (Lst (cons (hd Nat) (tl Lst)) (nil)))) + +(declare-fun app (Lst Lst) Lst) +(declare-fun rev (Lst) Lst) + +(declare-sort I_app 0) +(declare-sort I_rev 0) + +(declare-fun app_0_3 (I_app) Lst) +(declare-fun app_1_4 (I_app) Lst) +(declare-fun rev_0_5 (I_rev) Lst) + +(declare-fun xs () Lst) + +(assert (and + +(forall ((?i I_app)) (= (app (app_0_3 ?i) (app_1_4 ?i)) (ite (is-cons (app_0_3 ?i)) (cons (hd (app_0_3 ?i)) (app (tl (app_0_3 ?i)) (app_1_4 ?i))) (app_1_4 ?i))) ) + +(forall ((?i I_rev)) (= (rev (rev_0_5 ?i)) (ite (is-cons (rev_0_5 ?i)) (app (rev (tl (rev_0_5 ?i))) (cons (hd (rev_0_5 ?i)) nil)) nil)) ) + +(forall ((?i I_rev)) (or (not (is-cons (rev_0_5 ?i))) (and (not (forall ((?z I_app)) (not (and (= (app_0_3 ?z) (rev (tl (rev_0_5 ?i)))) (= (app_1_4 ?z) (cons (hd (rev_0_5 ?i)) nil)))) )) (not (forall ((?z I_rev)) (not (= (rev_0_5 ?z) (tl (rev_0_5 ?i)) )) )))) ) + +(not (or (= xs (rev xs)) (forall ((?z I_rev)) (not (= (rev_0_5 ?z) xs)) ))) + +)) + +(check-sat) + -- 2.30.2