diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/command.cpp | 84 | ||||
-rw-r--r-- | src/smt/command.h | 25 | ||||
-rw-r--r-- | src/smt/dump_manager.cpp | 1 | ||||
-rw-r--r-- | src/smt/listeners.cpp | 1 | ||||
-rw-r--r-- | src/smt/model.cpp | 6 | ||||
-rw-r--r-- | src/smt/model_blocker.h | 2 | ||||
-rw-r--r-- | src/smt/model_core_builder.h | 2 | ||||
-rw-r--r-- | src/smt/proof_manager.h | 1 | ||||
-rw-r--r-- | src/smt/quant_elim_solver.cpp | 14 | ||||
-rw-r--r-- | src/smt/quant_elim_solver.h | 13 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 14 |
11 files changed, 103 insertions, 60 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index e6361be9e..14b9ed0aa 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -29,7 +29,7 @@ #include "expr/expr_iomanip.h" #include "expr/node.h" #include "expr/symbol_manager.h" -#include "expr/type.h" +#include "expr/type_node.h" #include "options/options.h" #include "options/smt_options.h" #include "printer/printer.h" @@ -45,6 +45,43 @@ using namespace std; namespace CVC4 { +std::string sexprToString(api::Term sexpr) +{ + // if sexpr is a spec constant and not a string, return the result of calling + // Term::toString + if (sexpr.getKind() == api::CONST_BOOLEAN + || sexpr.getKind() == api::CONST_FLOATINGPOINT + || sexpr.getKind() == api::CONST_RATIONAL) + { + return sexpr.toString(); + } + + // if sexpr is a constant string, return the result of calling Term::toString. + // However, strip the surrounding quotes + if (sexpr.getKind() == api::CONST_STRING) + { + return sexpr.toString().substr(1, sexpr.toString().length() - 2); + } + + // if sexpr is not a spec constant, make sure it is an array of sub-sexprs + Assert(sexpr.getKind() == api::SEXPR); + + std::stringstream ss; + auto it = sexpr.begin(); + + // recursively print the sub-sexprs + ss << '(' << sexprToString(*it); + ++it; + while (it != sexpr.end()) + { + ss << ' ' << sexprToString(*it); + ++it; + } + ss << ')'; + + return ss.str(); +} + const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); const CommandInterrupted* CommandInterrupted::s_instance = @@ -137,11 +174,6 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) Command::Command() : d_commandStatus(nullptr), d_muted(false) {} -Command::Command(const api::Solver* solver) - : d_commandStatus(nullptr), d_muted(false) -{ -} - Command::Command(const Command& cmd) { d_commandStatus = @@ -1811,7 +1843,7 @@ void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->blockModelValues(d_terms); d_commandStatus = CommandSuccess::instance(); } - catch (RecoverableModalException& e) + catch (api::CVC4ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2520,21 +2552,21 @@ void SetBenchmarkLogicCommand::toStream(std::ostream& out, /* class SetInfoCommand */ /* -------------------------------------------------------------------------- */ -SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) +SetInfoCommand::SetInfoCommand(std::string flag, const std::string& sexpr) : d_flag(flag), d_sexpr(sexpr) { } std::string SetInfoCommand::getFlag() const { return d_flag; } -SExpr SetInfoCommand::getSExpr() const { return d_sexpr; } +const std::string& SetInfoCommand::getSExpr() const { return d_sexpr; } void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - solver->getSmtEngine()->setInfo(d_flag, d_sexpr); + solver->setInfo(d_flag, d_sexpr); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) + catch (api::CVC4ApiRecoverableException&) { // As per SMT-LIB spec, silently accept unknown set-info keys d_commandStatus = CommandSuccess::instance(); @@ -2570,23 +2602,13 @@ void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - vector<SExpr> v; - v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); - v.emplace_back(solver->getSmtEngine()->getInfo(d_flag)); - stringstream ss; - if (d_flag == "all-options" || d_flag == "all-statistics") - { - ss << PrettySExprs(true); - } - ss << SExpr(v); - d_result = ss.str(); + std::vector<api::Term> v; + v.push_back(solver->mkString(":" + d_flag)); + v.push_back(solver->mkString(solver->getInfo(d_flag))); + d_result = sexprToString(solver->mkTerm(api::SEXPR, v)); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) - { - d_commandStatus = new CommandUnsupported(); - } - catch (RecoverableModalException& e) + catch (api::CVC4ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2630,21 +2652,21 @@ void GetInfoCommand::toStream(std::ostream& out, /* class SetOptionCommand */ /* -------------------------------------------------------------------------- */ -SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) +SetOptionCommand::SetOptionCommand(std::string flag, const std::string& sexpr) : d_flag(flag), d_sexpr(sexpr) { } std::string SetOptionCommand::getFlag() const { return d_flag; } -SExpr SetOptionCommand::getSExpr() const { return d_sexpr; } +const std::string& SetOptionCommand::getSExpr() const { return d_sexpr; } void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - solver->getSmtEngine()->setOption(d_flag, d_sexpr); + solver->setOption(d_flag, d_sexpr); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) + catch (api::CVC4ApiRecoverableException&) { d_commandStatus = new CommandUnsupported(); } @@ -2682,7 +2704,7 @@ void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->getOption(d_flag); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) + catch (api::CVC4ApiRecoverableException&) { d_commandStatus = new CommandUnsupported(); } diff --git a/src/smt/command.h b/src/smt/command.h index 0b86f3539..bfe5e737a 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -29,8 +29,6 @@ #include <vector> #include "api/cvc4cpp.h" -#include "expr/expr.h" -#include "expr/type.h" #include "util/result.h" #include "util/sexpr.h" @@ -51,6 +49,16 @@ namespace smt { class Model; } +/** + * Convert a symbolic expression to string. This method differs from + * Term::toString in that it does not surround constant strings with double + * quote symbols. + * + * @param sexpr the symbolic expression to convert + * @return the symbolic expression as string + */ +std::string sexprToString(api::Term sexpr); + std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC; std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC4_PUBLIC; @@ -198,7 +206,6 @@ class CVC4_PUBLIC Command typedef CommandPrintSuccess printsuccess; Command(); - Command(const api::Solver* solver); Command(const Command& cmd); virtual ~Command(); @@ -1285,13 +1292,13 @@ class CVC4_PUBLIC SetInfoCommand : public Command { protected: std::string d_flag; - SExpr d_sexpr; + std::string d_sexpr; public: - SetInfoCommand(std::string flag, const SExpr& sexpr); + SetInfoCommand(std::string flag, const std::string& sexpr); std::string getFlag() const; - SExpr getSExpr() const; + const std::string& getSExpr() const; void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; @@ -1330,13 +1337,13 @@ class CVC4_PUBLIC SetOptionCommand : public Command { protected: std::string d_flag; - SExpr d_sexpr; + std::string d_sexpr; public: - SetOptionCommand(std::string flag, const SExpr& sexpr); + SetOptionCommand(std::string flag, const std::string& sexpr); std::string getFlag() const; - SExpr getSExpr() const; + const std::string& getSExpr() const; void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp index 9d3031b4d..51fcf8b5b 100644 --- a/src/smt/dump_manager.cpp +++ b/src/smt/dump_manager.cpp @@ -14,7 +14,6 @@ #include "smt/dump_manager.h" -#include "expr/expr_manager.h" #include "options/smt_options.h" #include "smt/dump.h" #include "smt/node_command.h" diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index 7d34f3373..356cfa8a6 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -15,7 +15,6 @@ #include "smt/listeners.h" #include "expr/attribute.h" -#include "expr/expr.h" #include "expr/node_manager_attributes.h" #include "options/smt_options.h" #include "printer/printer.h" diff --git a/src/smt/model.cpp b/src/smt/model.cpp index 8a9f944d2..ccf73dda0 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -49,7 +49,11 @@ Node Model::getValue(TNode n) const { return d_tmodel->getValue(n); } bool Model::hasApproximations() const { return d_tmodel->hasApproximations(); } -void Model::clearModelDeclarations() { d_declareSorts.clear(); } +void Model::clearModelDeclarations() +{ + d_declareTerms.clear(); + d_declareSorts.clear(); +} void Model::addDeclarationSort(TypeNode tn) { d_declareSorts.push_back(tn); } diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 92d200d40..5c45a6a56 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -19,7 +19,7 @@ #include <vector> -#include "expr/expr.h" +#include "expr/node.h" #include "options/smt_options.h" #include "theory/theory_model.h" diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h index 7a28c47f2..327933f1b 100644 --- a/src/smt/model_core_builder.h +++ b/src/smt/model_core_builder.h @@ -19,7 +19,7 @@ #include <vector> -#include "expr/expr.h" +#include "expr/node.h" #include "options/smt_options.h" #include "theory/theory_model.h" diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index 118b82bec..1916f0162 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -18,7 +18,6 @@ #define CVC4__SMT__PROOF_MANAGER_H #include "context/cdlist.h" -#include "expr/expr.h" #include "expr/node.h" #include "expr/proof_checker.h" #include "expr/proof_node.h" diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index e5ecafd4a..4636cf17a 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -14,6 +14,7 @@ #include "smt/quant_elim_solver.h" +#include "expr/skolem_manager.h" #include "expr/subs.h" #include "smt/smt_solver.h" #include "theory/quantifiers/cegqi/nested_qe.h" @@ -33,7 +34,8 @@ QuantElimSolver::~QuantElimSolver() {} Node QuantElimSolver::getQuantifierElimination(Assertions& as, Node q, - bool doFull) + bool doFull, + bool isInternalSubsolver) { Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl; if (q.getKind() != EXISTS && q.getKind() != FORALL) @@ -41,11 +43,13 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, throw ModalException( "Expecting a quantified formula as argument to get-qe."); } + NodeManager* nm = NodeManager::currentNM(); + // ensure the body is rewritten + q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1])); // do nested quantifier elimination if necessary q = quantifiers::NestedQe::doNestedQe(q, true); Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : " << q << std::endl; - NodeManager* nm = NodeManager::currentNM(); // tag the quantified formula with the quant-elim attribute TypeNode t = nm->booleanType(); Node n_attr = nm->mkSkolem("qe", t, "Auxiliary variable for qe attr."); @@ -121,6 +125,12 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, // do extended rewrite to minimize the size of the formula aggressively theory::quantifiers::ExtendedRewriter extr(true); ret = extr.extendedRewrite(ret); + // if we are not an internal subsolver, convert to witness form, since + // internally generated skolems should not escape + if (!isInternalSubsolver) + { + ret = SkolemManager::getWitnessForm(ret); + } return ret; } // otherwise, just true/false diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h index 96ed1f73d..ca55fc618 100644 --- a/src/smt/quant_elim_solver.h +++ b/src/smt/quant_elim_solver.h @@ -79,8 +79,19 @@ class QuantElimSolver * extended command get-qe-disjunct, which can be used * for incrementally computing the result of a * quantifier elimination. + * + * @param as The assertions of the SmtEngine + * @param q The quantified formula we are eliminating quantifiers from + * @param doFull Whether we are doing full quantifier elimination on q + * @param isInternalSubsolver Whether the SmtEngine we belong to is an + * internal subsolver. If it is not, then we convert the final result to + * witness form. + * @return The result of eliminating quantifiers from q. */ - Node getQuantifierElimination(Assertions& as, Node q, bool doFull); + Node getQuantifierElimination(Assertions& as, + Node q, + bool doFull, + bool isInternalSubsolver); private: /** The SMT solver, which is used during doQuantifierElimination. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0f40db530..2faad7961 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -332,6 +332,7 @@ SmtEngine::~SmtEngine() d_absValues.reset(nullptr); d_asserts.reset(nullptr); d_dumpm.reset(nullptr); + d_model.reset(nullptr); d_sygusSolver.reset(nullptr); @@ -468,11 +469,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) value.getValue() == "2.6" ) { ilang = language::input::LANG_SMTLIB_V2_6; } - else - { - Warning() << "Warning: unsupported smt-lib-version: " << value << endl; - throw UnrecognizedOptionException(); - } options::inputLanguage.set(ilang); // also update the output language if (!options::outputLanguage.wasSetByUser()) @@ -497,7 +493,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) d_state->notifyExpectedStatus(s); return; } - throw UnrecognizedOptionException(); } bool SmtEngine::isValidGetInfoFlag(const std::string& key) const @@ -517,10 +512,6 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const SmtScope smts(this); Trace("smt") << "SMT getInfo(" << key << ")" << endl; - if (!isValidGetInfoFlag(key)) - { - throw UnrecognizedOptionException(); - } if (key == "all-statistics") { vector<SExpr> stats; @@ -1508,7 +1499,8 @@ Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) if(!d_logic.isPure(THEORY_ARITH) && strict){ Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; } - return d_quantElimSolver->getQuantifierElimination(*d_asserts, q, doFull); + return d_quantElimSolver->getQuantifierElimination( + *d_asserts, q, doFull, d_isInternalSubsolver); } bool SmtEngine::getInterpol(const Node& conj, |