namespace cvc5 {
namespace smt {
-AbductionSolver::AbductionSolver(Env& env, SmtEngine* parent)
- : d_env(env), d_parent(parent)
-{
-}
+AbductionSolver::AbductionSolver(Env& env) : EnvObj(env) {}
AbductionSolver::~AbductionSolver() {}
-bool AbductionSolver::getAbduct(const Node& goal,
+bool AbductionSolver::getAbduct(const std::vector<Node>& axioms,
+ const Node& goal,
const TypeNode& grammarType,
Node& abd)
{
throw ModalException(msg);
}
Trace("sygus-abduct") << "SmtEngine::getAbduct: goal " << goal << std::endl;
- std::vector<Node> axioms = d_parent->getExpandedAssertions();
std::vector<Node> asserts(axioms.begin(), axioms.end());
// must expand definitions
Node conjn = d_env.getTopLevelSubstitutions().apply(goal);
d_subsolver->setLogic(l);
// assert the abduction query
d_subsolver->assertFormula(aconj);
- return getAbductInternal(abd);
+ return getAbductInternal(axioms, abd);
}
-bool AbductionSolver::getAbduct(const Node& goal, Node& abd)
+bool AbductionSolver::getAbduct(const std::vector<Node>& axioms,
+ const Node& goal,
+ Node& abd)
{
TypeNode grammarType;
- return getAbduct(goal, grammarType, abd);
+ return getAbduct(axioms, goal, grammarType, abd);
}
-bool AbductionSolver::getAbductInternal(Node& abd)
+bool AbductionSolver::getAbductInternal(const std::vector<Node>& axioms,
+ Node& abd)
{
// should have initialized the subsolver by now
Assert(d_subsolver != nullptr);
// if check abducts option is set, we check the correctness
if (options::checkAbducts())
{
- checkAbduct(abd);
+ checkAbduct(axioms, abd);
}
return true;
}
return false;
}
-void AbductionSolver::checkAbduct(Node a)
+void AbductionSolver::checkAbduct(const std::vector<Node>& axioms, Node a)
{
Assert(a.getType().isBoolean());
Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions"
<< std::endl;
- std::vector<Node> asserts = d_parent->getExpandedAssertions();
+ std::vector<Node> asserts(axioms.begin(), axioms.end());
asserts.push_back(a);
// two checks: first, consistent with assertions, second, implies negated goal
#include "expr/node.h"
#include "expr/type_node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
-class Env;
class SmtEngine;
namespace smt {
* a subsolver SmtEngine for a sygus conjecture that captures the abduction
* query, and implements supporting utility methods such as checkAbduct.
*/
-class AbductionSolver
+class AbductionSolver : protected EnvObj
{
public:
- AbductionSolver(Env& env, SmtEngine* parent);
+ AbductionSolver(Env& env);
~AbductionSolver();
/**
* This method asks this SMT engine to find an abduct with respect to the
* If this method returns true, then abd is set to a formula C such that
* A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable.
*
- * @param goal The goal of the abduction problem.
+ * @param axioms The expanded assertions A of the parent SMT engine
+ * @param goal The goal B of the abduction problem.
* @param grammarType A sygus datatype type that encodes the syntax
* restrictions on the shape of possible solutions.
- * @param abd This argument is updated to contain the solution to the
+ * @param abd This argument is updated to contain the solution C to the
* abduction problem. Notice that this is a formula whose free symbols
* are contained in goal + the parent's current assertion stack.
*
* This method invokes a separate copy of the SMT engine for solving the
* corresponding sygus problem for generating such a solution.
*/
- bool getAbduct(const Node& goal, const TypeNode& grammarType, Node& abd);
+ bool getAbduct(const std::vector<Node>& axioms,
+ const Node& goal,
+ const TypeNode& grammarType,
+ Node& abd);
/**
* Same as above, but without user-provided grammar restrictions. A default
* grammar is chosen internally using the sygus grammar constructor utility.
*/
- bool getAbduct(const Node& goal, Node& abd);
+ bool getAbduct(const std::vector<Node>& axioms, const Node& goal, Node& abd);
/**
* Check that a solution to an abduction conjecture is indeed a solution.
* solution to the abduction problem (a) is SAT, and the assertions conjoined
* with the abduct and the goal is UNSAT. If these criteria are not met, an
* internal error is thrown.
+ *
+ * @param axioms The expanded assertions of the parent SMT engine
+ * @param a The abduct to check.
*/
- void checkAbduct(Node a);
+ void checkAbduct(const std::vector<Node>& axioms, Node a);
private:
/**
* This method assumes d_subsolver has been initialized to do abduction
* problems.
*/
- bool getAbductInternal(Node& abd);
- /** Reference to the env */
- Env& d_env;
- /** The parent SMT engine */
- SmtEngine* d_parent;
+ bool getAbductInternal(const std::vector<Node>& axioms, Node& abd);
/** The SMT engine subsolver
*
* This is a separate copy of the SMT engine which is used for making
namespace cvc5 {
namespace smt {
-InterpolationSolver::InterpolationSolver(Env& env, SmtEngine* parent)
- : d_env(env), d_parent(parent)
-{
-}
+InterpolationSolver::InterpolationSolver(Env& env) : EnvObj(env) {}
InterpolationSolver::~InterpolationSolver() {}
-bool InterpolationSolver::getInterpol(const Node& conj,
+bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
+ const Node& conj,
const TypeNode& grammarType,
Node& interpol)
{
}
Trace("sygus-interpol") << "SmtEngine::getInterpol: conjecture " << conj
<< std::endl;
- std::vector<Node> axioms = d_parent->getExpandedAssertions();
// must expand definitions
Node conjn = d_env.getTopLevelSubstitutions().apply(conj);
std::string name("A");
return false;
}
-bool InterpolationSolver::getInterpol(const Node& conj, Node& interpol)
+bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
+ const Node& conj,
+ Node& interpol)
{
TypeNode grammarType;
- return getInterpol(conj, grammarType, interpol);
+ return getInterpol(axioms, conj, grammarType, interpol);
}
void InterpolationSolver::checkInterpol(Node interpol,
#include "expr/node.h"
#include "expr/type_node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
-
-class Env;
-class SmtEngine;
-
namespace smt {
/**
* a subsolver SmtEngine for a sygus conjecture that captures the interpolation
* query, and implements supporting utility methods such as checkInterpol.
*/
-class InterpolationSolver
+class InterpolationSolver : protected EnvObj
{
public:
- InterpolationSolver(Env& env, SmtEngine* parent);
+ InterpolationSolver(Env& env);
~InterpolationSolver();
/**
- * This method asks this SMT engine to find an interpolant with respect to
+ * This method asks this solver to find an interpolant with respect to
* the current assertion stack (call it A) and the conjecture (call it B). If
* this method returns true, then interpolant is set to a formula I such that
* A ^ ~I and I ^ ~B are both unsatisfiable.
*
- * @param conj The conjecture of the interpolation problem.
+ * @param axioms The expanded assertions A of the parent SMT engine
+ * @param conj The conjecture B of the interpolation problem.
* @param grammarType A sygus datatype type that encodes the syntax
* restrictions on the shape of possible solutions.
- * @param interpol This argument is updated to contain the solution to the
+ * @param interpol This argument is updated to contain the solution I to the
* interpolation problem.
*
* This method invokes a separate copy of the SMT engine for solving the
* corresponding sygus problem for generating such a solution.
*/
- bool getInterpol(const Node& conj,
+ bool getInterpol(const std::vector<Node>& axioms,
+ const Node& conj,
const TypeNode& grammarType,
Node& interpol);
* Same as above, but without user-provided grammar restrictions. A default
* grammar is chosen internally using the sygus grammar constructor utility.
*/
- bool getInterpol(const Node& conj, Node& interpol);
+ bool getInterpol(const std::vector<Node>& axioms,
+ const Node& conj,
+ Node& interpol);
/**
* Check that a solution to an interpolation problem is indeed a solution.
void checkInterpol(Node interpol,
const std::vector<Node>& easserts,
const Node& conj);
-
- private:
- /** Reference to the env */
- Env& d_env;
- /** The parent SMT engine */
- SmtEngine* d_parent;
};
} // namespace smt
// subsolvers
if (d_env->getOptions().smt.produceAbducts)
{
- d_abductSolver.reset(new AbductionSolver(*d_env.get(), this));
+ d_abductSolver.reset(new AbductionSolver(*d_env.get()));
}
if (d_env->getOptions().smt.produceInterpols
!= options::ProduceInterpols::NONE)
{
- d_interpolSolver.reset(new InterpolationSolver(*d_env.get(), this));
+ d_interpolSolver.reset(new InterpolationSolver(*d_env.get()));
}
d_pp->finishInit();
{
SmtScope smts(this);
finishInit();
- bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol);
+ std::vector<Node> axioms = getExpandedAssertions();
+ bool success =
+ d_interpolSolver->getInterpol(axioms, conj, grammarType, interpol);
// notify the state of whether the get-interpol call was successfuly, which
// impacts the SMT mode.
d_state->notifyGetInterpol(success);
{
SmtScope smts(this);
finishInit();
- bool success = d_abductSolver->getAbduct(conj, grammarType, abd);
+ std::vector<Node> axioms = getExpandedAssertions();
+ bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd);
// notify the state of whether the get-abduct call was successfuly, which
// impacts the SMT mode.
d_state->notifyGetAbduct(success);
projects / cvc5.git / commitdiff