diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-27 18:42:13 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-27 18:42:13 -0400 |
commit | 546e6aca016ea1f9b7da0bcfda5bed833a7a13ec (patch) | |
tree | f8722044b32d1360357a12034f5b919490f05456 | |
parent | b72ebc42011e4d55b28b807d362694447448c4e8 (diff) |
Some fixes to recent strings commits.
-rw-r--r-- | src/smt/smt_engine.cpp | 16 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 255 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 85 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 4 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop007.smt2 | 18 | ||||
-rw-r--r-- | 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; i<r.getNumChildren(); ++i) {
- Node sk = NodeManager::currentNM()->mkSkolem( "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; i<r.getNumChildren(); ++i) {
- simplifyRegExp( s, r[i], c_or );
- }
- Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or );
- ret.push_back( eq );
- }
- break;
- case kind::REGEXP_INTER:
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- simplifyRegExp( s, r[i], ret );
- }
- break;
- case kind::REGEXP_STAR:
- {
- Node sk = NodeManager::currentNM()->mkSkolem( "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; i<t.getNumChildren(); i++ ){
- Node tn = simplify( t[i] );
- cc.push_back( tn );
- changed = changed || tn!=t[i];
- }
- return changed ? NodeManager::currentNM()->mkNode( t.getKind(), cc ) : t;
- }else{
- return t;
- }
-}
-
-void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
- for( unsigned i=0; i<vec_node.size(); i++ ){
- vec_node[i] = simplify( vec_node[i] );
- }
-}
-
-}/* CVC4::theory::strings namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+/********************* */ +/*! \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; i<r.getNumChildren(); ++i) { + Node sk = NodeManager::currentNM()->mkSkolem( "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; i<r.getNumChildren(); ++i) { + simplifyRegExp( s, r[i], c_or ); + } + Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or ); + ret.push_back( eq ); + } + break; + case kind::REGEXP_INTER: + for(unsigned i=0; i<r.getNumChildren(); ++i) { + simplifyRegExp( s, r[i], ret ); + } + break; + case kind::REGEXP_STAR: + { + Node sk = NodeManager::currentNM()->mkSkolem( "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<TNode, Node, TNodeHashFunction>::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; i<t.getNumChildren(); i++ ){ + Node tn = simplify( t[i] ); + cc.push_back( tn ); + changed = changed || tn!=t[i]; + } + if(changed) { + Node n = NodeManager::currentNM()->mkNode( 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<vec_node.size(); i++ ){ + vec_node[i] = simplify( vec_node[i] ); + } +} + +}/* CVC4::theory::strings namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 2b2e7dfea..f82a3cf24 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -1,41 +1,44 @@ -/********************* */
-/*! \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 <vector>
-#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 <vector> +#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<TNode, Node, TNodeHashFunction> 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) |