return ret;
}
-BVGauss::BVGauss(PreprocessingPassContext* preprocContext)
- : PreprocessingPass(preprocContext, "bv-gauss")
+BVGauss::BVGauss(PreprocessingPassContext* preprocContext,
+ const std::string& name)
+ : PreprocessingPass(preprocContext, name)
{
}
class BVGauss : public PreprocessingPass
{
public:
- BVGauss(PreprocessingPassContext* preprocContext);
+ BVGauss(PreprocessingPassContext* preprocContext,
+ const std::string& name = "bv-gauss");
protected:
/**
#include "options/smt_options.h"
#include "smt/smt_statistics_registry.h"
+#include "theory/arith/arith_rewriter.h"
#include "theory/arith/infer_bounds.h"
#include "theory/arith/theory_arith_private.h"
#include "theory/ext_theory.h"
delete d_internal;
}
+std::unique_ptr<TheoryRewriter> TheoryArith::mkTheoryRewriter()
+{
+ return std::unique_ptr<TheoryRewriter>(new ArithRewriter());
+}
+
void TheoryArith::preRegisterTerm(TNode n){
d_internal->preRegisterTerm(n);
}
Valuation valuation, const LogicInfo& logicInfo);
virtual ~TheoryArith();
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
/**
* Does non-context dependent setup for a node connected to a theory.
*/
#include "smt/command.h"
#include "smt/logic_exception.h"
#include "smt/smt_statistics_registry.h"
+#include "theory/arrays/theory_arrays_rewriter.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"
#include "theory/valuation.h"
smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts);
}
+std::unique_ptr<TheoryRewriter> TheoryArrays::mkTheoryRewriter()
+{
+ return std::unique_ptr<TheoryRewriter>(new TheoryArraysRewriter());
+}
+
void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
std::string name = "");
~TheoryArrays();
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
std::string identify() const override { return std::string("TheoryArrays"); }
** The theory of booleans.
**/
-#include "theory/theory.h"
#include "theory/booleans/theory_bool.h"
-#include "theory/booleans/circuit_propagator.h"
-#include "theory/valuation.h"
-#include "smt_util/boolean_simplification.h"
-#include "theory/substitutions.h"
-#include <vector>
#include <stack>
+#include <vector>
+
+#include "smt_util/boolean_simplification.h"
+#include "theory/booleans/circuit_propagator.h"
+#include "theory/booleans/theory_bool_rewriter.h"
+#include "theory/substitutions.h"
+#include "theory/theory.h"
+#include "theory/valuation.h"
#include "util/hash.h"
using namespace std;
namespace theory {
namespace booleans {
+std::unique_ptr<TheoryRewriter> TheoryBool::mkTheoryRewriter()
+{
+ return std::unique_ptr<TheoryRewriter>(new TheoryBoolRewriter());
+}
+
Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) {
: Theory(THEORY_BOOL, c, u, out, valuation, logicInfo)
{}
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
//void check(Effort);
#include "theory/builtin/theory_builtin.h"
#include "expr/kind.h"
+#include "theory/builtin/theory_builtin_rewriter.h"
#include "theory/theory_model.h"
#include "theory/valuation.h"
{
}
+std::unique_ptr<TheoryRewriter> TheoryBuiltin::mkTheoryRewriter()
+{
+ return std::unique_ptr<TheoryRewriter>(new TheoryBuiltinRewriter());
+}
+
std::string TheoryBuiltin::identify() const
{
return std::string("TheoryBuiltin");
Valuation valuation,
const LogicInfo& logicInfo);
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
std::string identify() const override;
/** finish initialization */
TheoryBV::~TheoryBV() {}
+std::unique_ptr<TheoryRewriter> TheoryBV::mkTheoryRewriter()
+{
+ return std::unique_ptr<TheoryRewriter>(new TheoryBVRewriter());
+}
+
void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
if (options::bitblastMode() == options::BitblastMode::EAGER)
{
~TheoryBV();
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
void finishInit() override;
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "options/theory_options.h"
+#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/datatypes/theory_datatypes_type_rules.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers_engine.h"
}
}
+std::unique_ptr<TheoryRewriter> TheoryDatatypes::mkTheoryRewriter()
+{
+ return std::unique_ptr<TheoryRewriter>(new DatatypesRewriter());
+}
+
void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
const LogicInfo& logicInfo);
~TheoryDatatypes();
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
/** propagate */
** \todo document this file
**/
-
-#include "options/fp_options.h"
-#include "theory/rewriter.h"
-#include "theory/theory_model.h"
#include "theory/fp/theory_fp.h"
-
#include <set>
#include <stack>
#include <unordered_set>
#include <vector>
+#include "options/fp_options.h"
+#include "theory/fp/theory_fp_rewriter.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
+
using namespace std;
namespace CVC4 {
} /* TheoryFp::TheoryFp() */
+std::unique_ptr<TheoryRewriter> TheoryFp::mkTheoryRewriter()
+{
+ return std::unique_ptr<TheoryRewriter>(new TheoryFpRewriter());
+}
+
Node TheoryFp::minUF(Node node) {
Assert(node.getKind() == kind::FLOATINGPOINT_MIN);
TypeNode t(node.getType());
TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out,
Valuation valuation, const LogicInfo& logicInfo);
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
Node expandDefinition(LogicRequest& lr, Node node) override;
void preRegisterTerm(TNode node) override;
template=$1; shift
rewriter_includes=
-rewrite_init=
pre_rewrite_get_cache=
pre_rewrite_set_cache=
header="$2"
rewriter_includes="${rewriter_includes}#include \"$header\"
-"
- rewrite_init="${rewrite_init} d_theoryRewriters[${theory_id}].reset(new ${class});
"
pre_rewrite_attribute_ids="${pre_rewrite_attribute_ids} preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<${theory_id}>::pre_rewrite()));
"
post_rewrite_get_cache \
pre_rewrite_set_cache \
post_rewrite_set_cache \
- rewrite_init \
pre_rewrite_attribute_ids \
post_rewrite_attribute_ids \
template \
#include "theory/quantifiers/ematching/instantiation_engine.h"
#include "theory/quantifiers/fmf/model_engine.h"
#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
TheoryQuantifiers::~TheoryQuantifiers() {
}
+std::unique_ptr<TheoryRewriter> TheoryQuantifiers::mkTheoryRewriter()
+{
+ return std::unique_ptr<TheoryRewriter>(new QuantifiersRewriter());
+}
+
void TheoryQuantifiers::finishInit()
{
// quantifiers are not evaluated in getModelValue
const LogicInfo& logicInfo);
~TheoryQuantifiers();
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
/** finish initialization */
void finishInit() override;
void preRegisterTerm(TNode n) override;
return getInstance().rewriteTo(theoryOf(node), node);
}
+void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
+ std::unique_ptr<TheoryRewriter> trew)
+{
+ getInstance().d_theoryRewriters[tid] = std::move(trew);
+}
+
void Rewriter::registerPreRewrite(
Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
{
*/
static void clearCaches();
+ /**
+ * Registers a theory rewriter with this rewriter. This transfers the
+ * ownership of the theory rewriter to the rewriter.
+ *
+ * @param tid The theory that the theory rewriter should be associated with.
+ * @param trew The theory rewriter to register.
+ */
+ static void registerTheoryRewriter(theory::TheoryId tid,
+ std::unique_ptr<TheoryRewriter> trew);
+
/**
* Register a prerewrite for a given kind.
*
Rewriter::Rewriter()
{
-${rewrite_init}
-
for (size_t i = 0; i < kind::LAST_KIND; ++i)
{
d_preRewriters[i] = nullptr;
{
d_preRewritersEqual[i] = nullptr;
d_postRewritersEqual[i] = nullptr;
- d_theoryRewriters[i]->registerRewrites(this);
}
}
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
+#include "theory/sep/theory_sep_rewriter.h"
#include "theory/theory_model.h"
#include "theory/valuation.h"
}
}
+std::unique_ptr<TheoryRewriter> TheorySep::mkTheoryRewriter()
+{
+ return std::unique_ptr<TheoryRewriter>(new TheorySepRewriter());
+}
+
void TheorySep::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
~TheorySep();
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
std::string identify() const override { return std::string("TheorySep"); }
**/
#include "theory/sets/theory_sets.h"
+
#include "options/sets_options.h"
#include "theory/sets/theory_sets_private.h"
+#include "theory/sets/theory_sets_rewriter.h"
#include "theory/theory_model.h"
using namespace CVC4::kind;
// Do not move me to the header. See explanation in the constructor.
}
+std::unique_ptr<TheoryRewriter> TheorySets::mkTheoryRewriter()
+{
+ return std::unique_ptr<TheoryRewriter>(new TheorySetsRewriter());
+}
+
void TheorySets::finishInit()
{
TheoryModel* tm = d_valuation.getModel();
const LogicInfo& logicInfo);
~TheorySets() override;
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
/** finish initialization */
void finishInit() override;
void addSharedTerm(TNode) override;
#include "smt/smt_statistics_registry.h"
#include "theory/ext_theory.h"
#include "theory/rewriter.h"
+#include "theory/strings/sequences_rewriter.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/type_enumerator.h"
#include "theory/strings/word.h"
}
+std::unique_ptr<TheoryRewriter> TheoryStrings::mkTheoryRewriter()
+{
+ return std::unique_ptr<TheoryRewriter>(new SequencesRewriter());
+}
+
bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
Assert(d_equalityEngine.hasTerm(x));
Assert(d_equalityEngine.hasTerm(y));
const LogicInfo& logicInfo);
~TheoryStrings();
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
std::string identify() const override { return std::string("TheoryStrings"); }
#include "theory/logic_info.h"
#include "theory/output_channel.h"
#include "theory/theory_id.h"
+#include "theory/theory_rewriter.h"
#include "theory/valuation.h"
#include "util/statistics_registry.h"
*/
virtual ~Theory();
+ /**
+ * Creates a new theory rewriter for the theory.
+ */
+ virtual std::unique_ptr<TheoryRewriter> mkTheoryRewriter() = 0;
+
/**
* Subclasses of Theory may add additional efforts. DO NOT CHECK
* equality with one of these values (e.g. if STANDARD xxx) but
}
void TheoryEngine::finishInit() {
-
//initialize the quantifiers engine, master equality engine, model, model builder
if( d_logicInfo.isQuantified() ) {
// initialize the quantifiers engine
*d_theoryOut[theoryId],
theory::Valuation(this),
d_logicInfo);
+ theory::Rewriter::registerTheoryRewriter(
+ theoryId, d_theoryTable[theoryId]->mkTheoryRewriter());
}
void setPropEngine(prop::PropEngine* propEngine)
TheoryUF::~TheoryUF() {
}
+std::unique_ptr<TheoryRewriter> TheoryUF::mkTheoryRewriter()
+{
+ return std::unique_ptr<TheoryRewriter>(new TheoryUfRewriter());
+}
+
void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
~TheoryUF();
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
void finishInit() override;
d_nm = NodeManager::fromExprManager(d_em);
d_smt = new SmtEngine(d_em);
d_scope = new SmtScope(d_smt);
+ d_smt->finalOptionsAreSet();
d_zero = bv::utils::mkZero(16);
AssertionPipeline apipe;
apipe.push_back(a);
- passes::BVGauss bgauss(nullptr);
+ passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
std::unordered_map<Node, Node, NodeHashFunction> res;
PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
TS_ASSERT (pres == PreprocessingPassResult::NO_CONFLICT);
apipe.push_back(a);
apipe.push_back(eq4);
apipe.push_back(eq5);
- passes::BVGauss bgauss(nullptr);
+ passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
std::unordered_map<Node, Node, NodeHashFunction> res;
PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
TS_ASSERT (pres == PreprocessingPassResult::NO_CONFLICT);
AssertionPipeline apipe;
apipe.push_back(eq1);
apipe.push_back(eq2);
- passes::BVGauss bgauss(nullptr);
+ passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
std::unordered_map<Node, Node, NodeHashFunction> res;
PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
TS_ASSERT (pres == PreprocessingPassResult::NO_CONFLICT);
d_nm = NodeManager::fromExprManager(d_em);
d_smt = new SmtEngine(d_em);
d_scope = new SmtScope(d_smt);
+ d_smt->finalOptionsAreSet();
}
void tearDown() override
d_scope = new SmtScope(d_smt);
d_regExpOpr = new RegExpOpr();
+ // Ensure that the SMT engine is fully initialized (required for the
+ // rewriter)
+ d_smt->push();
+
d_nm = NodeManager::currentNM();
}
d_em = new ExprManager(opts);
d_smt = new SmtEngine(d_em);
d_scope = new SmtScope(d_smt);
+ d_smt->finalOptionsAreSet();
d_rewriter = new ExtendedRewriter(true);
d_nm = NodeManager::currentNM();
using namespace CVC4::smt;
class TheoryBlack : public CxxTest::TestSuite {
-private:
-
- ExprManager* d_em;
- SmtEngine* d_smt;
- NodeManager* d_nm;
- SmtScope* d_scope;
-
public:
void setUp() override
{
d_em = new ExprManager();
d_smt = new SmtEngine(d_em);
d_scope = new SmtScope(d_smt);
+ // Ensure that the SMT engine is fully initialized (required for the
+ // rewriter)
+ d_smt->push();
d_nm = NodeManager::fromExprManager(d_em);
}
}
+ private:
+ ExprManager* d_em;
+ SmtEngine* d_smt;
+ NodeManager* d_nm;
+ SmtScope* d_scope;
};
d_em = new ExprManager(opts);
d_smt = new SmtEngine(d_em);
d_scope = new SmtScope(d_smt);
+ d_smt->finalOptionsAreSet();
d_nm = NodeManager::currentNM();
}
#include "theory/rewriter.h"
#include "theory/theory.h"
#include "theory/theory_engine.h"
+#include "theory/theory_rewriter.h"
#include "theory/valuation.h"
#include "util/integer.h"
#include "util/proof.h"
bool d_topLevel;
};/* struct RewriteItem */
+class FakeTheoryRewriter : public TheoryRewriter
+{
+ public:
+ RewriteResponse preRewrite(TNode n) override
+ {
+ return RewriteResponse(REWRITE_DONE, n);
+ }
+
+ RewriteResponse postRewrite(TNode n) override
+ {
+ return RewriteResponse(REWRITE_DONE, n);
+ }
+};
+
/**
- * Fake Theory interface. Looks like a Theory, but really all it does is note when and
- * how rewriting behavior is requested.
+ * Fake Theory interface. Looks like a Theory, but really all it does is note
+ * when and how rewriting behavior is requested.
*/
-template<TheoryId theoryId>
-class FakeTheory : public Theory {
+template <TheoryId theoryId>
+class FakeTheory : public Theory
+{
/**
- * This fake theory class is equally useful for bool, uf, arith, etc. It keeps an
- * identifier to identify itself.
+ * This fake theory class is equally useful for bool, uf, arith, etc. It
+ * keeps an identifier to identify itself.
*/
std::string d_id;
/**
- * The expected sequence of rewrite calls. Filled by FakeTheory::expect() and consumed
- * by FakeTheory::preRewrite() and FakeTheory::postRewrite().
+ * The expected sequence of rewrite calls. Filled by FakeTheory::expect() and
+ * consumed by FakeTheory::preRewrite() and FakeTheory::postRewrite().
*/
// static std::deque<RewriteItem> s_expected;
-public:
- FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo)
- { }
-
- /** Register an expected rewrite call */
- static void expect(RewriteType type, FakeTheory* thy, TNode n, bool topLevel)
- throw()
+ public:
+ FakeTheory(context::Context* ctxt,
+ context::UserContext* uctxt,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo)
+ : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo)
{
- RewriteItem item = { type, thy, n, topLevel };
- //s_expected.push_back(item);
}
- /**
- * Returns whether the expected queue is empty. This is done after a call into
- * the rewriter to ensure that the actual set of observed rewrite calls completed
- * the sequence of expected rewrite calls.
- */
- static bool nothingMoreExpected() throw() {
- return true; // s_expected.empty();
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override
+ {
+ return std::unique_ptr<TheoryRewriter>(new FakeTheoryRewriter());
}
- /**
- * Overrides Theory::preRewrite(). This "fake theory" version ensures that
- * this actual, observed pre-rewrite call matches the next "expected" call set up
- * by the test.
- */
- RewriteResponse preRewrite(TNode n, bool topLevel) {
-// if(false) { //s_expected.empty()) {
-// cout << std::endl
-// << "didn't expect anything more, but got" << std::endl
-// << " PRE " << topLevel << " " << identify() << " " << n
-// << std::endl;
-// }
-// TS_ASSERT(!s_expected.empty());
-//
-// RewriteItem expected = s_expected.front();
-// s_expected.pop_front();
-//
-// if(expected.d_type != PRE ||
-//// expected.d_theory != this ||
-// expected.d_node != n ||
-// expected.d_topLevel != topLevel) {
-// cout << std::endl
-// << "HAVE PRE " << topLevel << " " << identify() << " " << n
-// << std::endl
-// << "WANT " << (expected.d_type == PRE ? "PRE " : "POST ")
-// // << expected.d_topLevel << " " << expected.d_theory->identify()
-// << " " << expected.d_node << std::endl << std::endl;
-// }
-//
-// TS_ASSERT_EQUALS(expected.d_type, PRE);
-//// TS_ASSERT_EQUALS(expected.d_theory, this);
-// TS_ASSERT_EQUALS(expected.d_node, n);
-// TS_ASSERT_EQUALS(expected.d_topLevel, topLevel);
-
- return RewriteResponse(REWRITE_DONE, n);
+ /** Register an expected rewrite call */
+ static void expect(RewriteType type,
+ FakeTheory* thy,
+ TNode n,
+ bool topLevel) throw()
+ {
+ RewriteItem item = {type, thy, n, topLevel};
+ // s_expected.push_back(item);
}
/**
- * Overrides Theory::postRewrite(). This "fake theory" version ensures that
- * this actual, observed post-rewrite call matches the next "expected" call set up
- * by the test.
+ * Returns whether the expected queue is empty. This is done after a call
+ * into the rewriter to ensure that the actual set of observed rewrite calls
+ * completed the sequence of expected rewrite calls.
*/
- RewriteResponse postRewrite(TNode n, bool topLevel) {
-// if(s_expected.empty()) {
-// cout << std::endl
-// << "didn't expect anything more, but got" << std::endl
-// << " POST " << topLevel << " " << identify() << " " << n
-// << std::endl;
-// }
-// TS_ASSERT(!s_expected.empty());
-//
-// RewriteItem expected = s_expected.front();
-// s_expected.pop_front();
-//
-// if(expected.d_type != POST ||
-//// expected.d_theory != this ||
-// expected.d_node != n ||
-// expected.d_topLevel != topLevel) {
-// cout << std::endl
-// << "HAVE POST " << topLevel << " " << identify() << " " << n
-// << std::endl
-// << "WANT " << (expected.d_type == PRE ? "PRE " : "POST ")
-//// << expected.d_topLevel << " " << expected.d_theory->identify()
-// << " " << expected.d_node << std::endl << std::endl;
-// }
-//
-// TS_ASSERT_EQUALS(expected.d_type, POST);
-// TS_ASSERT_EQUALS(expected.d_theory, this);
-// TS_ASSERT_EQUALS(expected.d_node, n);
-// TS_ASSERT_EQUALS(expected.d_topLevel, topLevel);
-
- return RewriteResponse(REWRITE_DONE, n);
+ static bool nothingMoreExpected() throw()
+ {
+ return true; // s_expected.empty();
}
std::string identify() const override {
return Node::null();
}
Node getValue(TNode n) { return Node::null(); }
-};/* class FakeTheory */
-
+}; /* class FakeTheory */
/* definition of the s_expected static field in FakeTheory; see above */
// std::deque<RewriteItem> FakeTheory::s_expected;
d_nm = NodeManager::fromExprManager(d_em);
d_smt = new SmtEngine(d_em);
d_scope = new SmtScope(d_smt);
+ d_smt->finalOptionsAreSet();
}
void BvInstantiatorWhite::tearDown()
#include <cxxtest/TestSuite.h>
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "theory/sets/theory_sets_type_enumerator.h"
using namespace CVC4;
+using namespace CVC4::smt;
using namespace CVC4::theory;
using namespace CVC4::kind;
using namespace CVC4::theory::sets;
class SetEnumeratorWhite : public CxxTest::TestSuite
{
- ExprManager* d_em;
- NodeManager* d_nm;
- NodeManagerScope* d_scope;
-
public:
void setUp() override
{
d_em = new ExprManager();
+ d_smt = new SmtEngine(d_em);
d_nm = NodeManager::fromExprManager(d_em);
- d_scope = new NodeManagerScope(d_nm);
+ d_scope = new SmtScope(d_smt);
+ d_smt->finalOptionsAreSet();
}
void tearDown() override
{
delete d_scope;
+ delete d_smt;
delete d_em;
}
TS_ASSERT_EQUALS(expected2, actual2);
TS_ASSERT(!setEnumerator.isFinished());
- Node actual3 = *++setEnumerator;
- Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2);
+ Node actual3 = Rewriter::rewrite(*++setEnumerator);
+ Node expected3 =
+ Rewriter::rewrite(d_nm->mkNode(Kind::UNION, expected1, expected2));
TS_ASSERT_EQUALS(expected3, actual3);
TS_ASSERT(!setEnumerator.isFinished());
TS_ASSERT(setEnumerator.isFinished());
}
+ private:
+ ExprManager* d_em;
+ SmtEngine* d_smt;
+ NodeManager* d_nm;
+ SmtScope* d_scope;
}; /* class SetEnumeratorWhite */
#include <memory>
+#include "expr/expr_manager.h"
#include "expr/node.h"
#include "expr/node_manager.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "theory/strings/skolem_cache.h"
#include "util/rational.h"
#include "util/string.h"
using namespace CVC4;
+using namespace CVC4::smt;
using namespace CVC4::theory::strings;
class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite
public:
void setUp() override
{
- d_nm.reset(new NodeManager(nullptr));
- d_scope.reset(new NodeManagerScope(d_nm.get()));
+ d_em.reset(new ExprManager());
+ d_smt.reset(new SmtEngine(d_em.get()));
+ d_scope.reset(new SmtScope(d_smt.get()));
+ // Ensure that the SMT engine is fully initialized (required for the
+ // rewriter)
+ d_smt->push();
+
+ d_nm = NodeManager::fromExprManager(d_em.get());
}
void tearDown() override {}
}
private:
- std::unique_ptr<NodeManager> d_nm;
- std::unique_ptr<NodeManagerScope> d_scope;
+ std::unique_ptr<ExprManager> d_em;
+ std::unique_ptr<SmtEngine> d_smt;
+ NodeManager* d_nm;
+ std::unique_ptr<SmtScope> d_scope;
};
};
class DummyTheory : public Theory {
-public:
+ public:
set<Node> d_registered;
vector<Node> d_getSequence;
: Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo)
{}
+ std::unique_ptr<TheoryRewriter> mkTheoryRewriter()
+ {
+ return std::unique_ptr<TheoryRewriter>();
+ }
+
void registerTerm(TNode n) {
// check that we registerTerm() a term only once
TS_ASSERT(d_registered.find(n) == d_registered.end());
#include "expr/node_manager.h"
#include "expr/type_node.h"
#include "options/language.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "theory/type_enumerator.h"
using namespace CVC4;
+using namespace CVC4::smt;
using namespace CVC4::theory;
using namespace CVC4::kind;
using namespace std;
class TypeEnumeratorWhite : public CxxTest::TestSuite {
- ExprManager* d_em;
- NodeManager* d_nm;
- NodeManagerScope* d_scope;
-
public:
void setUp() override
{
d_em = new ExprManager();
+ d_smt = new SmtEngine(d_em);
d_nm = NodeManager::fromExprManager(d_em);
- d_scope = new NodeManagerScope(d_nm);
+ d_scope = new SmtScope(d_smt);
+ d_smt->finalOptionsAreSet();
}
void tearDown() override
{
delete d_scope;
+ delete d_smt;
delete d_em;
}
TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
}
+ private:
+ ExprManager* d_em;
+ SmtEngine* d_smt;
+ NodeManager* d_nm;
+ SmtScope* d_scope;
};/* class TypeEnumeratorWhite */
projects / cvc5.git / commitdiff