summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/command.cpp84
-rw-r--r--src/smt/command.h25
-rw-r--r--src/smt/dump_manager.cpp1
-rw-r--r--src/smt/listeners.cpp1
-rw-r--r--src/smt/model.cpp6
-rw-r--r--src/smt/model_blocker.h2
-rw-r--r--src/smt/model_core_builder.h2
-rw-r--r--src/smt/proof_manager.h1
-rw-r--r--src/smt/quant_elim_solver.cpp14
-rw-r--r--src/smt/quant_elim_solver.h13
-rw-r--r--src/smt/smt_engine.cpp14
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,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback