bug fix in strings : change from assert to alwaysassert

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index fe7b9b3d935e46c88d02204b793ad090cf0b7a4b..f4fbd7194be9bd91d4a44e84a6df4a63003c3ce8 100644 (file)
--- 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 3fceb06d4459cbfd027d61a6840c93c8e7f97445..2832c7833df32cb3da7666a930662b2a700482be 100644 (file)
--- 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 4876b54e7ccbbba7ec0e64dec3da63d433a3b5f2..1aae55a8361028546b30489409dabec5232af1cb 100644 (file)
--- 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 d043f06ecffc814e2a67c04b31b09e063731ea5e..7f2dce5aebb2608af1748f305f087cf3354b7884 100644 (file)
--- 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