From 8f0aae827e16f4dfcebb8dad2cc528649d40b16a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 21 Mar 2018 08:03:48 -0500 Subject: Fix for string disequality processing (#1679) --- src/theory/strings/theory_strings.cpp | 26 +++++++++++++++++++------- 1 file changed, 19 insertions(+), 7 deletions(-) (limited to 'src/theory/strings/theory_strings.cpp') 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; + } } } } -- cgit v1.2.3