From: ajreynol Date: Fri, 20 May 2016 22:10:03 +0000 (-0500) Subject: Minor fix to strings, cleanup in datatypes. X-Git-Tag: cvc5-1.0.0~6049^2~40 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=453ae55ac7adcda70b4dfbc95c78e899961c8e2d;p=cvc5.git Minor fix to strings, cleanup in datatypes. --- diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 89ba3c6a7..0100f1833 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -56,8 +56,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, //d_consEqc( c ), d_conflict( c, false ), d_collectTermsCache( c ), - d_consTerms( c ), - d_selTerms( c ), + d_functionTerms( c ), d_singleton_eq( u ), d_lemmas_produced_c( u ) { @@ -1352,36 +1351,32 @@ void TheoryDatatypes::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers:: void TheoryDatatypes::computeCareGraph(){ unsigned n_pairs = 0; - Trace("dt-cg-summary") << "Compute graph for dt..." << d_consTerms.size() << " " << d_selTerms.size() << " " << d_sharedTerms.size() << std::endl; + Trace("dt-cg-summary") << "Compute graph for dt..." << d_functionTerms.size() << " " << d_sharedTerms.size() << std::endl; Trace("dt-cg") << "Build indices..." << std::endl; std::map< TypeNode, std::map< Node, quantifiers::TermArgTrie > > index; std::map< Node, unsigned > arity; //populate indices - for( unsigned r=0; r<2; r++ ){ - unsigned functionTerms = r==0 ? d_consTerms.size() : d_selTerms.size(); - for( unsigned i=0; i0 ){ - Assert(d_equalityEngine.hasTerm(f1)); - Trace("dt-cg-debug") << "...build for " << f1 << std::endl; - //break into index based on operator, and type of first argument (since some operators are parametric) - Node op = f1.getOperator(); - TypeNode tn = f1[0].getType(); - std::vector< TNode > reps; - bool has_trigger_arg = false; - for( unsigned j=0; j reps; + bool has_trigger_arg = false; + for( unsigned j=0; j >::iterator iti = index.begin(); iti != index.end(); ++iti ){ @@ -1607,11 +1602,13 @@ void TheoryDatatypes::collectTerms( Node n ) { //} if( n.getKind() == APPLY_CONSTRUCTOR ){ Debug("datatypes") << " Found constructor " << n << endl; - d_consTerms.push_back( n ); + if( n.getNumChildren()>0 ){ + d_functionTerms.push_back( n ); + } }else{ if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE || n.getKind() == DT_HEIGHT_BOUND ){ - d_selTerms.push_back( n ); + d_functionTerms.push_back( n ); //we must also record which selectors exist Trace("dt-collapse-sel") << " Found selector " << n << endl; Node rep = getRepresentative( n[0] ); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index f3963f972..a1882d171 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -181,10 +181,8 @@ private: std::vector< Node > d_pending; std::map< Node, Node > d_pending_exp; std::vector< Node > d_pending_merge; - /** All the constructor terms that the theory has seen */ - context::CDList d_consTerms; - /** All the selector terms that the theory has seen */ - context::CDList d_selTerms; + /** All the function terms that the theory has seen */ + context::CDList d_functionTerms; /** counter for forcing assignments (ensures fairness) */ unsigned d_dtfCounter; /** expand definition skolem functions */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 52d71a8a9..f2af6452b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -456,11 +456,6 @@ void TheoryStrings::preRegisterTerm(TNode n) { ss << "Term of kind " << n.getKind() << " not supported in default mode, try --strings-exp"; throw LogicException(ss.str()); } - }else{ - //collect extended functions here: some may not be asserted to strings (such as those with return type Int), - // but we need to record them so they are treated properly - std::map< Node, bool > visited; - collectExtendedFuncTerms( n, visited ); } switch( n.getKind() ) { case kind::EQUAL: { @@ -475,19 +470,26 @@ void TheoryStrings::preRegisterTerm(TNode n) { break; } default: { - if( n.getType().isString() ) { + TypeNode tn = n.getType(); + if( tn.isString() ) { registerTerm( n, 0 ); // FMF if( n.getKind() == kind::VARIABLE && options::stringFMF() ){ d_input_vars.insert(n); } d_equalityEngine.addTerm(n); - } else if (n.getType().isBoolean()) { + } else if (tn.isBoolean()) { // Get triggered for both equal and dis-equal d_equalityEngine.addTriggerPredicate(n); } else { // Function applications/predicates d_equalityEngine.addTerm(n); + if( options::stringExp() ){ + //collect extended functions here: some may not be asserted to strings (such as those with return type Int), + // but we need to record them so they are treated properly + std::map< Node, bool > visited; + collectExtendedFuncTerms( n, visited ); + } } //concat terms do not contribute to theory combination? TODO: verify if( n.hasOperator() && kindToTheoryId( n.getKind() )==THEORY_STRINGS && n.getKind()!=kind::STRING_CONCAT ){ @@ -499,6 +501,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { } Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) { + Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl; return node; } diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 771b9f031..3daf646ab 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -76,7 +76,8 @@ TESTS = \ type002.smt2 \ crash-1019.smt2 \ norn-31.smt2 \ - strings-native-simple.cvc + strings-native-simple.cvc \ + cmu-2db2-extf-reg.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 b/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 new file mode 100644 index 000000000..b513494b8 --- /dev/null +++ b/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun s () String) + +(assert (and (not (not (= (ite (= (str.indexof s "bar" 1) (- 1)) 1 0) 0))) (not (not (= (ite (= (str.indexof s "bar" 1) 3) 1 0) 0))))) + +(check-sat)