diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 66 |
1 files changed, 40 insertions, 26 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d1b18df13..942c8d216 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -38,8 +38,9 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, pnm), d_notify(*this), d_statistics(), d_equalityEngine(d_notify, c, "theory::strings::ee", true), @@ -189,18 +190,20 @@ bool TheoryStrings::propagate(TNode literal) { return ok; } - -Node TheoryStrings::explain( TNode literal ){ +TrustNode TheoryStrings::explain(TNode literal) +{ Debug("strings-explain") << "explain called on " << literal << std::endl; std::vector< TNode > assumptions; d_im->explain(literal, assumptions); + Node ret; if( assumptions.empty() ){ - return d_true; + ret = d_true; }else if( assumptions.size()==1 ){ - return assumptions[0]; + ret = assumptions[0]; }else{ - return NodeManager::currentNM()->mkNode( kind::AND, assumptions ); + ret = NodeManager::currentNM()->mkNode(kind::AND, assumptions); } + return TrustNode::mkTrustPropExp(literal, ret, nullptr); } bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& vars, @@ -577,7 +580,7 @@ void TheoryStrings::preRegisterTerm(TNode n) d_termReg.preRegisterTerm(n); } -Node TheoryStrings::expandDefinition(Node node) +TrustNode TheoryStrings::expandDefinition(Node node) { Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl; @@ -593,14 +596,15 @@ Node TheoryStrings::expandDefinition(Node node) Node k = nm->mkBoundVar(nm->stringType()); Node bvl = nm->mkNode(BOUND_VAR_LIST, k); Node emp = Word::mkEmptyWord(node.getType()); - node = nm->mkNode( + Node ret = nm->mkNode( WITNESS, bvl, nm->mkNode( ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp))); + return TrustNode::mkTrustRewrite(node, ret, nullptr); } - return node; + return TrustNode::null(); } void TheoryStrings::check(Effort e) { @@ -712,11 +716,12 @@ void TheoryStrings::conflict(TNode a, TNode b){ { Debug("strings-conflict") << "Making conflict..." << std::endl; d_state.setConflict(); - Node conflictNode; - conflictNode = explain( a.eqNode(b) ); - Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl; + TrustNode conflictNode = explain(a.eqNode(b)); + Trace("strings-conflict") + << "CONFLICT: Eq engine conflict : " << conflictNode.getNode() + << std::endl; ++(d_statistics.d_conflictsEqEngine); - d_out->conflict( conflictNode ); + d_out->conflict(conflictNode.getNode()); } } @@ -957,39 +962,48 @@ void TheoryStrings::checkRegisterTermsNormalForms() } } -Node TheoryStrings::ppRewrite(TNode atom) { +TrustNode TheoryStrings::ppRewrite(TNode atom) +{ Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl; - Node atomElim; + Node atomRet = atom; if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP) { // aggressive elimination of regular expression membership - atomElim = d_regexp_elim.eliminate(atom); + Node atomElim = d_regexp_elim.eliminate(atomRet); if (!atomElim.isNull()) { Trace("strings-ppr") << " rewrote " << atom << " -> " << atomElim << " via regular expression elimination." << std::endl; - atom = atomElim; + atomRet = atomElim; } } if( !options::stringLazyPreproc() ){ //eager preprocess here std::vector< Node > new_nodes; StringsPreprocess* p = d_esolver->getPreprocess(); - Node ret = p->processAssertion(atom, new_nodes); - if( ret!=atom ){ - Trace("strings-ppr") << " rewrote " << atom << " -> " << ret << ", with " << new_nodes.size() << " lemmas." << std::endl; - for( unsigned i=0; i<new_nodes.size(); i++ ){ - Trace("strings-ppr") << " lemma : " << new_nodes[i] << std::endl; + Node ret = p->processAssertion(atomRet, new_nodes); + if (ret != atomRet) + { + Trace("strings-ppr") << " rewrote " << atomRet << " -> " << ret + << ", with " << new_nodes.size() << " lemmas." + << std::endl; + for (const Node& lem : new_nodes) + { + Trace("strings-ppr") << " lemma : " << lem << std::endl; ++(d_statistics.d_lemmasEagerPreproc); - d_out->lemma( new_nodes[i] ); + d_out->lemma(lem); } - return ret; + atomRet = ret; }else{ Assert(new_nodes.empty()); } } - return atom; + if (atomRet != atom) + { + return TrustNode::mkTrustRewrite(atom, atomRet, nullptr); + } + return TrustNode::null(); } /** run the given inference step */ |