diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-21 08:03:48 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-21 08:03:48 -0500 |
| commit | 8f0aae827e16f4dfcebb8dad2cc528649d40b16a (patch) | |
| tree | 5fe4cfd49013cb0f46ea4641099b66083bb1e9a4 | |
| parent | 614670f98a9ab2d3cfcb9f364a1b06d78f63ebb0 (diff) | |
Fix for string disequality processing (#1679)
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 26 | ||||
| -rw-r--r-- | test/regress/regress1/strings/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress1/strings/goodAI.smt2 | 8 |
3 files changed, 29 insertions, 8 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 81b0118c5..b5a4370d4 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3142,13 +3142,25 @@ int TheoryStrings::processReverseDeq( std::vector< Node >& nfi, std::vector< Nod } int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ){ - //see if one side is constant, if so, we can approximate as containment - for( unsigned i=0; i<2; i++ ){ - Node c = getConstantEqc( i==0 ? ni : nj ); - if( !c.isNull() ){ - int findex, lindex; - if( !TheoryStringsRewriter::canConstantContainList( c, i==0 ? nfj : nfi, findex, lindex ) ){ - return 1; + // See if one side is constant, if so, the disequality ni != nj is satisfied + // since ni does not contain nj or vice versa. + // This is only valid when isRev is false, since when isRev=true, the contents + // of normal form vectors nfi and nfj are reversed. + if (!isRev) + { + for (unsigned i = 0; i < 2; i++) + { + Node c = getConstantEqc(i == 0 ? ni : nj); + if (!c.isNull()) + { + int findex, lindex; + if (!TheoryStringsRewriter::canConstantContainList( + c, i == 0 ? nfj : nfi, findex, lindex)) + { + Trace("strings-solve-debug") + << "Disequality: constant cannot contain list" << std::endl; + return 1; + } } } } diff --git a/test/regress/regress1/strings/Makefile.am b/test/regress/regress1/strings/Makefile.am index f6326e0c6..7e9242e73 100644 --- a/test/regress/regress1/strings/Makefile.am +++ b/test/regress/regress1/strings/Makefile.am @@ -73,7 +73,8 @@ TESTS = \ str007.smt2 \ rew-020618.smt2 \ double-replace.smt2 \ - string-unsound-sem.smt2 + string-unsound-sem.smt2 \ + goodAI.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress1/strings/goodAI.smt2 b/test/regress/regress1/strings/goodAI.smt2 new file mode 100644 index 000000000..0dc5c8ab1 --- /dev/null +++ b/test/regress/regress1/strings/goodAI.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_S) +(set-option :strings-exp true) +(set-info :status sat) +(declare-const input_0_1000 String) +(assert (= (str.substr input_0_1000 0 4) "good")) +(assert (= (str.substr input_0_1000 5 1) "I")) +(assert (not (= input_0_1000 "goodAI"))) +(check-sat) |