diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-30 17:18:10 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-30 17:18:24 +0200 |
commit | f2da7296ff76920528c0e9edc35f96a715b85078 (patch) | |
tree | 21c7b56ab3f0216f1444b454d2671a5e60c9a0d4 /src/theory/quantifiers_engine.cpp | |
parent | f1dfab159ff9b29bfe86e976ae9953d77eefa308 (diff) |
Implement virtual term substitution for non-nested quantifiers. Fix soundness bug in strings related to explaining length terms.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 54f2a16fe..06fc8898b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -599,15 +599,21 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No } } -bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){ +bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){ Assert( f.getKind()==FORALL ); Assert( vars.size()==terms.size() ); Node body = getInstantiation( f, vars, terms ); + //do virtual term substitution + if( doVts ){ + body = Rewriter::rewrite( body ); + Trace("inst-debug") << "Rewrite vts symbols in " << body << std::endl; + Node body_r = d_term_db->rewriteVtsSymbols( body ); + Trace("inst-debug") << " ...result: " << body_r << std::endl; + body = body_r; + } Trace("inst-assert") << "(assert " << body << ")" << std::endl; //make the lemma - NodeBuilder<> nb(kind::OR); - nb << f.notNode() << body; - Node lem = nb; + Node lem = NodeManager::currentNM()->mkNode( kind::OR, f.negate(), body ); //check for duplication if( addLemma( lem ) ){ d_total_inst_debug[f]++; @@ -805,13 +811,13 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ d_phase_req_waiting[lit] = req; } -bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){ +bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst, bool doVts ){ std::vector< Node > terms; m.getTerms( this, f, terms ); - return addInstantiation( f, terms, mkRep, modEq, modInst ); + return addInstantiation( f, terms, mkRep, modEq, modInst, doVts ); } -bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) { +bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) { // For resource-limiting (also does a time check). getOutputChannel().safePoint(options::quantifierStep()); @@ -875,7 +881,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo //add the instantiation Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; - bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms ); + bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms, doVts ); //report the result if( addedInst ){ Trace("inst-add-debug") << " -> Success." << std::endl; |