diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 186 |
1 files changed, 128 insertions, 58 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 007c5e049..3dc64d61a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -955,6 +955,45 @@ public: std::ostream* getReplayLog() const { return d_managedReplayLog.getReplayLog(); } + + Node replaceQuantifiersWithInstantiations( Node n, std::map< Node, std::vector< Node > >& insts, std::map< Node, Node >& visited ){ + std::map< Node, Node >::iterator itv = visited.find( n ); + if( itv!=visited.end() ){ + return itv->second; + }else{ + Node ret = n; + if( n.getKind()==kind::FORALL ){ + std::map< Node, std::vector< Node > >::iterator it = insts.find( n ); + if( it==insts.end() ){ + Trace("smt-qe-debug") << "* " << n << " has no instances" << std::endl; + ret = NodeManager::currentNM()->mkConst(true); + }else{ + Trace("smt-qe-debug") << "* " << n << " has " << it->second.size() << " instances" << std::endl; + Node reti = it->second.empty() ? NodeManager::currentNM()->mkConst(true) : ( it->second.size()==1 ? it->second[0] : NodeManager::currentNM()->mkNode( kind::AND, it->second ) ); + Trace("smt-qe-debug") << " return : " << ret << std::endl; + //recursive (for nested quantification) + ret = replaceQuantifiersWithInstantiations( reti, insts, visited ); + } + }else if( n.getNumChildren()>0 ){ + bool childChanged = false; + std::vector< Node > children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node r = replaceQuantifiersWithInstantiations( n[i], insts, visited ); + children.push_back( r ); + childChanged = childChanged || r!=n[i]; + } + if( childChanged ){ + ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + } + visited[n] = ret; + return ret; + } + } + };/* class SmtEnginePrivate */ }/* namespace CVC4::smt */ @@ -4318,80 +4357,80 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce Trace("smt") << "SMT query(" << ex << ")" << endl; try { - if(d_queryMade && !options::incrementalSolving()) { - throw ModalException("Cannot make multiple queries unless " - "incremental solving is enabled " - "(try --incremental)"); - } + if(d_queryMade && !options::incrementalSolving()) { + throw ModalException("Cannot make multiple queries unless " + "incremental solving is enabled " + "(try --incremental)"); + } - // Substitute out any abstract values in ex - Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); - // Ensure that the expression is type-checked at this point, and Boolean - ensureBoolean(e); + // Substitute out any abstract values in ex + Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); + // Ensure that the expression is type-checked at this point, and Boolean + ensureBoolean(e); - // check to see if a postsolve() is pending - if(d_needPostsolve) { - d_theoryEngine->postsolve(); - d_needPostsolve = false; - } + // check to see if a postsolve() is pending + if(d_needPostsolve) { + d_theoryEngine->postsolve(); + d_needPostsolve = false; + } - // Push the context - internalPush(); + // Push the context + internalPush(); - // Note that a query has been made - d_queryMade = true; + // Note that a query has been made + d_queryMade = true; - // Add the formula - d_problemExtended = true; - if(d_assertionList != NULL) { - d_assertionList->push_back(e.notExpr()); - } - d_private->addFormula(e.getNode().notNode(), inUnsatCore); + // Add the formula + d_problemExtended = true; + if(d_assertionList != NULL) { + d_assertionList->push_back(e.notExpr()); + } + d_private->addFormula(e.getNode().notNode(), inUnsatCore); - // Run the check - Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - r = check().asValidityResult(); - d_needPostsolve = true; + // Run the check + Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); + r = check().asValidityResult(); + d_needPostsolve = true; - // Dump the query if requested - if(Dump.isOn("benchmark")) { - // the expr already got dumped out if assertion-dumping is on - Dump("benchmark") << QueryCommand(ex); - } + // Dump the query if requested + if(Dump.isOn("benchmark")) { + // the expr already got dumped out if assertion-dumping is on + Dump("benchmark") << QueryCommand(ex); + } - // Pop the context - internalPop(); + // Pop the context + internalPop(); - // Remember the status - d_status = r; + // Remember the status + d_status = r; - d_problemExtended = false; + d_problemExtended = false; - Trace("smt") << "SMT query(" << e << ") ==> " << r << endl; + Trace("smt") << "SMT query(" << e << ") ==> " << r << endl; - // Check that SAT results generate a model correctly. - if(options::checkModels()) { - if(r.asSatisfiabilityResult().isSat() == Result::SAT || - (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){ - checkModel(/* hard failure iff */ ! r.isUnknown()); + // Check that SAT results generate a model correctly. + if(options::checkModels()) { + if(r.asSatisfiabilityResult().isSat() == Result::SAT || + (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){ + checkModel(/* hard failure iff */ ! r.isUnknown()); + } } - } - // Check that UNSAT results generate a proof correctly. - if(options::checkProofs()) { - if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { - TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); - checkProof(); + // Check that UNSAT results generate a proof correctly. + if(options::checkProofs()) { + if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); + checkProof(); + } } - } - // Check that UNSAT results generate an unsat core correctly. - if(options::checkUnsatCores()) { - if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { - TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime); - checkUnsatCore(); + // Check that UNSAT results generate an unsat core correctly. + if(options::checkUnsatCores()) { + if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime); + checkUnsatCore(); + } } - } - return r; + return r; } catch (UnsafeInterruptException& e) { AlwaysAssert(d_private->getResourceManager()->out()); Result::UnknownExplanation why = d_private->getResourceManager()->outOfResources() ? @@ -5017,6 +5056,37 @@ void SmtEngine::printSynthSolution( std::ostream& out ) { } } +Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull) { + SmtScope smts(this); + Trace("smt-qe") << "Do quantifier elimination " << e << std::endl; + Result r = query(e); + Trace("smt-qe") << "Query returned " << r << std::endl; + if(r.asSatisfiabilityResult().isSat() == Result::SAT) { + Node input = Node::fromExpr( e ); + input = Rewriter::rewrite( input ); + Trace("smt-qe") << "Replace instances in rewritten input: " << input << std::endl; + std::map< Node, std::vector< Node > > insts; + d_theoryEngine->getInstantiations( insts ); + std::map< Node, Node > visited; + Node en = d_private->replaceQuantifiersWithInstantiations( input, insts, visited ); + + //ensure all instantiations were accounted for + for( std::map< Node, std::vector< Node > >::iterator it = insts.begin(); it != insts.end(); ++it ){ + if( visited.find( it->first )==visited.end() ){ + stringstream ss; + ss << "While performing quantifier elimination, processed a quantified formula : " << it->first; + ss << " that was not related to the query. Try option --simplification=none." << std::endl; + InternalError(ss.str().c_str()); + } + } + Trace("smt-qe") << "Returned : " << en << std::endl; + en = Rewriter::rewrite( en ); + return en.toExpr(); + }else{ + return NodeManager::currentNM()->mkConst(false).toExpr(); + } +} + vector<Expr> SmtEngine::getAssertions() throw(ModalException) { SmtScope smts(this); finalOptionsAreSet(); |