adds fmf for strings

3 files changed, 67 insertions, 17 deletions

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<TNode>& 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 */