diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-01 10:47:31 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-01 10:47:47 -0600 |
commit | ffaf556b34e3ef2972b47caea00b7da149aeea8f (patch) | |
tree | 0fd3616edf9aed8447bce1ffaa5e444d8824e43c /src/theory | |
parent | 154002c3a1b07ead16cfcac05a7580abc424e472 (diff) |
Improvement and bug fix for str.indexof reduction, add regression. Other minor changes.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 6 | ||||
-rw-r--r-- | src/theory/sep/kinds | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 16 |
3 files changed, 13 insertions, 11 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 1a0faa021..20f5eae7b 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -231,7 +231,11 @@ int ModelEngine::checkModel(){ } bool ModelEngine::considerQuantifiedFormula( Node q ) { - if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) || !d_quantEngine->getModel()->isQuantifierActive( q ) ){ + if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){ + Trace("model-engine-debug") << "Model builder inactive : " << q << std::endl; + return false; + }else if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){ + Trace("model-engine-debug") << "Model inactive : " << q << std::endl; return false; }else{ if( options::fmfEmptySorts() ){ diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds index 318442ba5..5cd9093f4 100644 --- a/src/theory/sep/kinds +++ b/src/theory/sep/kinds @@ -25,7 +25,7 @@ operator SEP_EMP 2 "separation empty heap" operator SEP_PTO 2 "points to relation" operator SEP_STAR 2: "separation star" operator SEP_WAND 2 "separation magic wand" -operator SEP_LABEL 2 "separation label" +operator SEP_LABEL 2 "separation label (internal use only)" typerule SEP_NIL_REF ::CVC4::theory::sep::SepNilRefTypeRule typerule SEP_EMP ::CVC4::theory::sep::SepEmpTypeRule diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index a697dad75..c8fe1fb00 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -116,25 +116,23 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" ); } Node st = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, t[0], t[2], NodeManager::currentNM()->mkNode( kind::MINUS, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), t[2] ) ); + //TODO: simplify this (only applies when idof != -1) Node eq = st.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk2, sk3, sk4 ) ); new_nodes.push_back( eq ); + + //learn range of idof? Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); Node krange = NodeManager::currentNM()->mkNode( kind::GEQ, skk, negone ); new_nodes.push_back( krange ); krange = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk); new_nodes.push_back( krange ); - krange = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] ), d_zero); - new_nodes.push_back( krange ); - Node start_valid = NodeManager::currentNM()->mkNode( kind::GEQ, t[2], d_zero); - //str.len(s1) < y + str.len(s2) - Node c1 = NodeManager::currentNM()->mkNode( kind::GT, - NodeManager::currentNM()->mkNode( kind::PLUS, t[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] )), - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] )); + // s2 = "" + Node c1 = t[1].eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); //~contain(t234, s2) Node c3 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, st, t[1] ).negate(); //left - Node left = NodeManager::currentNM()->mkNode( kind::OR, c1, c3, start_valid.negate() ); + Node left = NodeManager::currentNM()->mkNode( kind::OR, c1, c3 ); //t3 = s2 Node c4 = t[1].eqNode( sk3 ); //~contain(t2, s2) @@ -149,7 +147,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node c6 = skk.eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, t[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 )) ); //right - Node right = NodeManager::currentNM()->mkNode( kind::AND, c4, c5, c6, start_valid ); + Node right = NodeManager::currentNM()->mkNode( kind::AND, c4, c5, c6, c1.negate() ); Node cond = skk.eqNode( negone ); Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right ); new_nodes.push_back( rr ); |