From 546e6aca016ea1f9b7da0bcfda5bed833a7a13ec Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 27 Sep 2013 18:42:13 -0400 Subject: [PATCH] Some fixes to recent strings commits. --- src/smt/smt_engine.cpp | 16 +- .../strings/theory_strings_preprocess.cpp | 255 +++++++++--------- .../strings/theory_strings_preprocess.h | 85 +++--- .../strings/theory_strings_type_rules.h | 4 +- src/theory/theory_engine.cpp | 2 +- test/regress/regress0/strings/loop007.smt2 | 18 +- test/regress/regress0/strings/model001.smt2 | 24 +- 7 files changed, 211 insertions(+), 193 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index df568f1ab..39ccc70c4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -988,8 +988,8 @@ void SmtEngine::setLogicInternal() throw() { ) || // Quantifiers d_logic.isQuantified() || - // Strings - d_logic.isTheoryEnabled(THEORY_STRINGS) + // Strings + d_logic.isTheoryEnabled(THEORY_STRINGS) ? decision::DECISION_STRATEGY_JUSTIFICATION : decision::DECISION_STRATEGY_INTERNAL ); @@ -1008,7 +1008,7 @@ void SmtEngine::setLogicInternal() throw() { d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed() ) || // Quantifiers - d_logic.isQuantified() + d_logic.isQuantified() ? true : false ); @@ -2861,12 +2861,12 @@ void SmtEnginePrivate::processAssertions() { // Assertions ARE guaranteed to be rewritten by this point - if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ){ - CVC4::theory::strings::StringsPreprocess sp; - sp.simplify( d_assertionsToPreprocess ); + if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { + CVC4::theory::strings::StringsPreprocess sp; + sp.simplify( d_assertionsToPreprocess ); for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] ); - } + d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] ); + } } dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess); diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index d62fd4c9e..8fa4345e5 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -1,120 +1,135 @@ -/********************* */ -/*! \file theory_strings_preprocess.cpp - ** \verbatim - ** Original author: Tianyi Liang - ** Major contributors: Tianyi Liang, Andrew Reynolds - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2013-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Strings Preprocess - ** - ** Strings Preprocess. - **/ - -#include "theory/strings/theory_strings_preprocess.h" -#include "expr/kind.h" - -namespace CVC4 { -namespace theory { -namespace strings { - -void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) { - int k = r.getKind(); - switch( k ) { - case kind::STRING_TO_REGEXP: - { - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] ); - ret.push_back( eq ); - } - break; - case kind::REGEXP_CONCAT: - { - std::vector< Node > cc; - for(unsigned i=0; imkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" ); - simplifyRegExp( sk, r[i], ret ); - cc.push_back( sk ); - } - Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) ); - ret.push_back( cc_eq ); - } - break; - case kind::REGEXP_OR: - { - std::vector< Node > c_or; - for(unsigned i=0; imkNode( kind::OR, c_or ); - ret.push_back( eq ); - } - break; - case kind::REGEXP_INTER: - for(unsigned i=0; imkSkolem( "ressym_$$", s.getType(), "created for regular expression star" ); - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, s ), - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, sk )); - ret.push_back( eq ); - simplifyRegExp( sk, r[0], ret ); - } - break; - case kind::REGEXP_OPT: - { - Node eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); - std::vector< Node > rr; - simplifyRegExp( s, r[0], rr ); - Node nrr = rr.size()==1 ? rr[0] : NodeManager::currentNM()->mkNode( kind::AND, rr ); - ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) ); - } - break; - default: - //TODO:case kind::REGEXP_PLUS: - //TODO: special sym: sigma, none, all - break; - } -} - -Node StringsPreprocess::simplify( Node t ) { - if( t.getKind() == kind::STRING_IN_REGEXP ){ - // t0 in t1 - //rewrite it - std::vector< Node > ret; - simplifyRegExp( t[0], t[1], ret ); - - return ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret ); - }else if( t.getNumChildren()>0 ){ - std::vector< Node > cc; - if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { - cc.push_back(t.getOperator()); - } - bool changed = false; - for( unsigned i=0; imkNode( t.getKind(), cc ) : t; - }else{ - return t; - } -} - -void StringsPreprocess::simplify(std::vector< Node > &vec_node) { - for( unsigned i=0; i &ret ) { + int k = r.getKind(); + switch( k ) { + case kind::STRING_TO_REGEXP: + { + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] ); + ret.push_back( eq ); + } + break; + case kind::REGEXP_CONCAT: + { + std::vector< Node > cc; + for(unsigned i=0; imkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" ); + simplifyRegExp( sk, r[i], ret ); + cc.push_back( sk ); + } + Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) ); + ret.push_back( cc_eq ); + } + break; + case kind::REGEXP_OR: + { + std::vector< Node > c_or; + for(unsigned i=0; imkNode( kind::OR, c_or ); + ret.push_back( eq ); + } + break; + case kind::REGEXP_INTER: + for(unsigned i=0; imkSkolem( "ressym_$$", s.getType(), "created for regular expression star" ); + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, s ), + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, sk )); + ret.push_back( eq ); + simplifyRegExp( sk, r[0], ret ); + } + break; + case kind::REGEXP_OPT: + { + Node eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); + std::vector< Node > rr; + simplifyRegExp( s, r[0], rr ); + Node nrr = rr.size()==1 ? rr[0] : NodeManager::currentNM()->mkNode( kind::AND, rr ); + ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) ); + } + break; + default: + //TODO:case kind::REGEXP_PLUS: + //TODO: special sym: sigma, none, all + break; + } +} + +Node StringsPreprocess::simplify( Node t ) { + std::hash_map::const_iterator i = d_cache.find(t); + if(i != d_cache.end()) { + return (*i).second.isNull() ? t : (*i).second; + } + + if( t.getKind() == kind::STRING_IN_REGEXP ){ + // t0 in t1 + //rewrite it + std::vector< Node > ret; + simplifyRegExp( t[0], t[1], ret ); + + Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret ); + d_cache[t] = (t == n) ? Node::null() : n; + return n; + }else if( t.getNumChildren()>0 ){ + std::vector< Node > cc; + if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { + cc.push_back(t.getOperator()); + } + bool changed = false; + for( unsigned i=0; imkNode( t.getKind(), cc ); + d_cache[t] = n; + return n; + } else { + d_cache[t] = Node::null(); + return t; + } + }else{ + d_cache[t] = Node::null(); + return t; + } +} + +void StringsPreprocess::simplify(std::vector< Node > &vec_node) { + for( unsigned i=0; i -#include "theory/theory.h" - -namespace CVC4 { -namespace theory { -namespace strings { - -class StringsPreprocess { -private: - void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); - Node simplify( Node t ); -public: -void simplify(std::vector< Node > &vec_node); -}; - -}/* CVC4::theory::strings namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__STRINGS__PREPROCESS_H */ +/********************* */ +/*! \file theory_strings_preprocess.h + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: Tianyi Liang, Andrew Reynolds + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2013-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Strings Preprocess + ** + ** Strings Preprocess. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__STRINGS__PREPROCESS_H +#define __CVC4__THEORY__STRINGS__PREPROCESS_H + +#include +#include "util/hash.h" +#include "theory/theory.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +class StringsPreprocess { + // NOTE: this class is NOT context-dependent + std::hash_map d_cache; +private: + void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); + Node simplify( Node t ); +public: +void simplify(std::vector< Node > &vec_node); +}; + +}/* CVC4::theory::strings namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__STRINGS__PREPROCESS_H */ diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 9c3d6c71e..8fc630206 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -181,9 +181,9 @@ public: if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting string terms"); } - if( (*it).getKind() != kind::CONST_STRING ) { + if( (*it).getKind() != kind::CONST_STRING ) { throw TypeCheckingExceptionPrivate(n, "expecting constant string terms"); - } + } if(++it != it_end) { throw TypeCheckingExceptionPrivate(n, "too many terms"); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d4f08fcdd..78710e4b9 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -371,7 +371,7 @@ void TheoryEngine::check(Theory::Effort effort) { // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) { - //d_theoryTable[THEORY_STRINGS]->check(Theory::EFFORT_LAST_CALL); + //d_theoryTable[THEORY_STRINGS]->check(Theory::EFFORT_LAST_CALL); if(d_logicInfo.isQuantified()) { // quantifiers engine must pass effort last call check d_quantEngine->check(Theory::EFFORT_LAST_CALL); diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2 index 8d789edb3..0534d8b53 100644 --- a/test/regress/regress0/strings/loop007.smt2 +++ b/test/regress/regress0/strings/loop007.smt2 @@ -1,10 +1,10 @@ -(set-logic ALL_SUPPORTED) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun y () String) - -(assert (= (str.++ x y "aa") (str.++ "aa" y x))) -(assert (= (str.len x) 1)) - +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) + +(assert (= (str.++ x y "aa") (str.++ "aa" y x))) +(assert (= (str.len x) 1)) + (check-sat) \ No newline at end of file diff --git a/test/regress/regress0/strings/model001.smt2 b/test/regress/regress0/strings/model001.smt2 index e4e35f40d..2832b5c96 100644 --- a/test/regress/regress0/strings/model001.smt2 +++ b/test/regress/regress0/strings/model001.smt2 @@ -1,12 +1,12 @@ -(set-logic ALL_SUPPORTED) -(set-info :status sat) -(set-option :produce-models true) - -(declare-fun x () String) -(declare-fun y () String) - -(assert (not (= x y))) -(assert (= (str.len x) (str.len y))) - -(check-sat) -;(get-model) +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) + +(declare-fun x () String) +(declare-fun y () String) + +(assert (not (= x y))) +(assert (= (str.len x) (str.len y))) + +(check-sat) +;(get-model) -- 2.30.2