bug fix in strings : change from assert to alwaysassert

4 files changed, 29 insertions, 13 deletions

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index fe7b9b3d9..f4fbd7194 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -3,7 +3,7 @@
 
 theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h"
 
-properties check parametric propagate
+properties check parametric propagate getNextDecisionRequest
 
 rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_strings_rewriter.h"
 
diff --git a/src/theory/strings/options b/src/theory/strings/options
index 3fceb06d4..2832c7833 100644
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -6,9 +6,12 @@
 module STRINGS "theory/strings/options.h" Strings theory
 
 option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :default 256 :read-write
- the cardinality of the characters used by the theory of string, default 256
+ the cardinality of the characters used by the theory of strings, default 256
 
 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 string, default 10
+ the depth of unrolloing regular expression used by the theory of strings, default 10
+
+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 4876b54e7..1aae55a83 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -61,6 +61,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
 
 	//option
 	d_regexp_unroll_depth = options::stringRegExpUnrollDepth();
+	d_fmf = options::stringFMF();
 }
 
 TheoryStrings::~TheoryStrings() {
@@ -343,6 +344,12 @@ void TheoryStrings::preRegisterTerm(TNode n) {
 		  Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl;
 		  d_out->lemma(n_len_geq_zero);
 	  }
+	  // FMF
+	  if( d_fmf && 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 );
+		  }
+	  }
     }
     if (n.getType().isBoolean()) {
       // Get triggered for both equal and dis-equal
@@ -1343,7 +1350,7 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an )
         } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ){
             Assert( hasTerm(a[i][0][0]) );
             Assert( hasTerm(a[i][0][1]) );
-            Assert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
+            AlwaysAssert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
         }
 		if( exp ){
 			unsigned ps = antec_exp.size();
@@ -1900,18 +1907,20 @@ bool TheoryStrings::checkMemberships() {
 	}
 }
 
-/*
 Node TheoryStrings::getNextDecisionRequest() {
-	if( d_lit_to_decide_index.get()<d_lit_to_decide.size() ){
-		Node l = d_lit_to_decide[d_lit_to_decide_index.get()];
-		d_lit_to_decide_index.set( d_lit_to_decide_index.get() + 1 );
-		Trace("strings-ind") << "Strings-ind : decide on " << l << std::endl;
-		return l;
-	}else{
-		return Node::null();
+	if(d_fmf) {
+		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) {
+				Trace("strings-fmf-debug") << " " << (*itr) ;
+			}
+		Trace("strings-fmf-debug") << std::endl;
 	}
+
+	return Node::null();
 }
-*/
+
 }/* 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 d043f06ec..7f2dce5ae 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -60,6 +60,7 @@ 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
@@ -126,6 +127,9 @@ 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