From 7284a228b22fb82740faf2abdfe5cb3fc3894ae9 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 16 Oct 2013 13:24:56 -0500 Subject: [PATCH] adds fmf for strings --- src/theory/strings/options | 2 +- src/theory/strings/theory_strings.cpp | 64 +++++++++++++++++++---- src/theory/strings/theory_strings.h | 18 +++++-- test/regress/regress0/strings/Makefile.am | 1 + test/regress/regress0/strings/fmf001.smt2 | 19 +++++++ 5 files changed, 87 insertions(+), 17 deletions(-) create mode 100644 test/regress/regress0/strings/fmf001.smt2 diff --git a/src/theory/strings/options b/src/theory/strings/options index 58cbbc1b1..2832c7833 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -11,7 +11,7 @@ option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :de option stringRegExpUnrollDepth str-regexp-depth --str-regexp-depth=N int16_t :default 10 :read-write the depth of unrolloing regular expression used by the theory of strings, default 10 -option stringFMF strings-fmf --str-fmf bool :default false +option stringFMF fmf-strings --fmf-strings bool :default false the finite model finding used by the theory of strings endmodule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index c4ecd02cf..8bff4dddc 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -47,7 +47,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu //d_ind_map_lemma(c), //d_lit_to_decide_index( c, 0 ), //d_lit_to_decide( c ), - d_reg_exp_mem( c ) + d_reg_exp_mem( c ), + d_curr_cardinality( c, 0 ) { // The kinds we are treating as function application in congruence //d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); @@ -61,7 +62,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu //option d_regexp_unroll_depth = options::stringRegExpUnrollDepth(); - d_fmf = options::stringFMF(); + //d_fmf = options::stringFMF(); } TheoryStrings::~TheoryStrings() { @@ -345,7 +346,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { d_out->lemma(n_len_geq_zero); } // FMF - if( d_fmf && n.getKind() == kind::VARIABLE ) { + if( options::stringFMF() && n.getKind() == kind::VARIABLE ) { if( std::find(d_in_vars.begin(), d_in_vars.end(), n) == d_in_vars.end() ) { d_in_vars.push_back( n ); } @@ -1908,21 +1909,62 @@ bool TheoryStrings::checkMemberships() { } Node TheoryStrings::getNextDecisionRequest() { - if(d_fmf && !d_conflict) { - Trace("strings-decide") << "Get next decision request." << std::endl; - Trace("strings-fmf-debug") << "Input variables: "; - for(std::vector< Node >::iterator itr = d_in_vars.begin(); - itr != d_in_vars.end(); ++itr) { + if(options::stringFMF() && !d_conflict) { + //initialize the term we will minimize + if( d_in_var_lsum.isNull() && !d_in_vars.empty() ){ + Trace("strings-fmf-debug") << "Input variables: "; + std::vector< Node > ll; + for(std::vector< Node >::iterator itr = d_in_vars.begin(); + itr != d_in_vars.end(); ++itr) { Trace("strings-fmf-debug") << " " << (*itr) ; + ll.push_back( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr ) ); } - Trace("strings-fmf-debug") << std::endl; - - + Trace("strings-fmf-debug") << std::endl; + d_in_var_lsum = ll.size()==1 ? ll[0] : NodeManager::currentNM()->mkNode( kind::PLUS, ll ); + d_in_var_lsum = Rewriter::rewrite( d_in_var_lsum ); + } + if( !d_in_var_lsum.isNull() ){ + //Trace("strings-fmf") << "Get next decision request." << std::endl; + //check if we need to decide on something + int decideCard = d_curr_cardinality.get(); + if( d_cardinality_lits.find( decideCard )!=d_cardinality_lits.end() ){ + bool value; + if( d_valuation.hasSatValue( d_cardinality_lits[ d_curr_cardinality.get() ], value ) ) { + if( !value ){ + d_curr_cardinality.set( d_curr_cardinality.get() + 1 ); + decideCard = d_curr_cardinality.get(); + Trace("strings-fmf-debug") << "Has false SAT value, increment and decide." << std::endl; + }else{ + decideCard = -1; + Trace("strings-fmf-debug") << "Has true SAT value, do not decide." << std::endl; + } + }else{ + Trace("strings-fmf-debug") << "No SAT value, decide." << std::endl; + } + } + if( decideCard!=-1 ){ + if( d_cardinality_lits.find( decideCard )==d_cardinality_lits.end() ){ + Node lit = NodeManager::currentNM()->mkNode( kind::LEQ, d_in_var_lsum, NodeManager::currentNM()->mkConst( Rational( decideCard ) ) ); + lit = Rewriter::rewrite( lit ); + d_cardinality_lits[decideCard] = lit; + Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() ); + Trace("strings-fmf") << "Strings FMF: Add split lemma " << lem << ", decideCard = " << decideCard << std::endl; + d_out->lemma( lem ); + d_out->requirePhase( lit, true ); + } + Trace("strings-fmf") << "Strings FMF: Decide positive on " << d_cardinality_lits[ decideCard ] << std::endl; + return d_cardinality_lits[ decideCard ]; + } + } } return Node::null(); } +void TheoryStrings::assertNode( Node lit ) { + +} + }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 7f2dce5ae..69875edf4 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -60,7 +60,6 @@ class TheoryStrings : public Theory { bool propagate(TNode literal); void explain( TNode literal, std::vector& assumptions ); Node explain( TNode literal ); - Node getNextDecisionRequest(); // NotifyClass for equality engine @@ -127,9 +126,6 @@ class TheoryStrings : public Theory { Node d_true; Node d_false; Node d_zero; - // Finite Model Finding - bool d_fmf; - std::vector< Node > d_in_vars; // RegExp depth int d_regexp_unroll_depth; //list of pairs of nodes to merge @@ -249,8 +245,20 @@ protected: //seperate into collections with equal length void seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts ); -private: void printConcat( std::vector< Node >& n, const char * c ); + +private: + // Finite Model Finding + //bool d_fmf; + std::vector< Node > d_in_vars; + Node d_in_var_lsum; + std::map< int, Node > d_cardinality_lits; + context::CDO< int > d_curr_cardinality; +public: + //for finite model finding + Node getNextDecisionRequest(); + void assertNode( Node lit ); + };/* class TheoryStrings */ }/* CVC4::theory::strings namespace */ diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 49a431796..ffbfb077d 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -26,6 +26,7 @@ TESTS = \ str004.smt2 \ str005.smt2 \ str006.smt2 \ + fmf001.smt2 \ model001.smt2 \ substr001.smt2 \ regexp001.smt2 \ diff --git a/test/regress/regress0/strings/fmf001.smt2 b/test/regress/regress0/strings/fmf001.smt2 new file mode 100644 index 000000000..a8874b59f --- /dev/null +++ b/test/regress/regress0/strings/fmf001.smt2 @@ -0,0 +1,19 @@ +(set-logic QF_S) +(set-option :fmf-strings true) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) + +(assert (str.in.re x + (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) + )) + +(assert (str.in.re y + (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) + )) + +(assert (not (= x y))) +(assert (= (str.len x) (str.len y))) + +(check-sat) -- 2.30.2