I also expect this commit to fix bug #273.
No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
+(cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1
# We descend into "src" with the "check" target here to ensure that
# the test prerequisites are all built.
-units: all
+units:
(cd src && $(MAKE) $(AM_MAKEFLAGS) check)
+(cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1
check test units:
(cd $(CURRENT_BUILD)/src && $(MAKE) check)
+(cd $(CURRENT_BUILD)/test && $(MAKE) $@)
-systemtests regress:
+systemtests regress: all
+(cd $(CURRENT_BUILD)/test && $(MAKE) $@)
units%:
(cd $(CURRENT_BUILD)/src && $(MAKE) check)
return d_map.size();
}
+ bool empty() const {
+ return d_map.empty();
+ }
+
size_t count(const Key& k) const {
return d_map.count(k);
}
friend std::ostream&
operator<<(std::ostream&, const Context&) throw(AssertionException);
+ // disable copy, assignment
+ Context(const Context&) CVC4_UNUSED;
+ Context& operator=(const Context&) CVC4_UNUSED;
+
public:
/**
* Constructor: create ContextMemoryManager and initial Scope
};/* class Context */
+
+/**
+ * A UserContext is different from a Context only because it's used for
+ * different purposes---so separating the two types gives type errors where
+ * appropriate.
+ */
+class UserContext : public Context {
+private:
+ // disable copy, assignment
+ UserContext(const UserContext&) CVC4_UNUSED;
+ UserContext& operator=(const UserContext&) CVC4_UNUSED;
+public:
+ UserContext() {}
+};/* class UserContext */
+
+
/**
* Conceptually, a Scope encapsulates that portion of the context that
* changes after a call to push() and must be undone on a subsequent call to
namespace CVC4 {
ExprManager::ExprManager() :
- d_ctxt(new Context),
+ d_ctxt(new Context()),
d_nodeManager(new NodeManager(d_ctxt, this)) {
#ifdef CVC4_STATISTICS_ON
for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
}
ExprManager::ExprManager(const Options& options) :
- d_ctxt(new Context),
+ d_ctxt(new Context()),
d_nodeManager(new NodeManager(d_ctxt, this, options)) {
#ifdef CVC4_STATISTICS_ON
for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
**/
#include <iostream>
+#include <cstdlib>
#include <vector>
#include <string>
#include <set>
if(d_in == cin) {
::rl_readline_name = "CVC4";
::rl_completion_entry_function = commandGenerator;
+ ::using_history();
switch(OutputLanguage lang = toOutputLanguage(d_language)) {
case output::LANG_CVC4:
+ d_historyFilename = string(getenv("HOME")) + "/.cvc4_history";
commandsBegin = cvc_commands;
commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
break;
case output::LANG_SMTLIB:
+ d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib";
commandsBegin = smt_commands;
commandsEnd = smt_commands + sizeof(smt_commands) / sizeof(*smt_commands);
break;
case output::LANG_SMTLIB_V2:
+ d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
commandsBegin = smt2_commands;
commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
break;
default: Unhandled(lang);
}
d_usingReadline = true;
+ int err = ::read_history(d_historyFilename.c_str());
+ ::stifle_history(s_historyLimit);
+ if(Notice.isOn()) {
+ if(err == 0) {
+ Notice() << "Read " << ::history_length << " lines of history from "
+ << d_historyFilename << std::endl;
+ } else {
+ Notice() << "Could not read history from " << d_historyFilename
+ << ": " << strerror(err) << std::endl;
+ }
+ }
} else {
d_usingReadline = false;
}
#endif /* HAVE_LIBREADLINE */
}/* InteractiveShell::InteractiveShell() */
+InteractiveShell::~InteractiveShell() {
+ int err = ::write_history(d_historyFilename.c_str());
+ if(err == 0) {
+ Notice() << "Wrote " << ::history_length << " lines of history to "
+ << d_historyFilename << std::endl;
+ } else {
+ Notice() << "Could not write history to " << d_historyFilename
+ << ": " << strerror(err) << std::endl;
+ }
+}
Command* InteractiveShell::readCommand() {
/* Don't do anything if the input is closed or if we've seen a
bool d_quit;
bool d_usingReadline;
+ std::string d_historyFilename;
+
static const std::string INPUT_FILENAME;
+ static const unsigned s_historyLimit = 500;
public:
InteractiveShell(ExprManager& exprManager, const Options& options);
+ /**
+ * Close out the interactive session.
+ */
+ ~InteractiveShell();
+
/**
* Read a command from the interactive shell. This will read as
* many lines as necessary to parse a well-formed command.
ok = false;
// Cancel the trail downto previous push
- popTrail();
+ //popTrail();
return status;
}
class SmtEnginePrivate {
SmtEngine& d_smt;
- /** The assertions yet to be preprecessed */
+ /** The assertions yet to be preprocessed */
vector<Node> d_assertionsToPreprocess;
/** Learned literals */
public:
- SmtEnginePrivate(SmtEngine& smt) : d_smt(smt) { }
+ SmtEnginePrivate(SmtEngine& smt) :
+ d_smt(smt),
+ d_topLevelSubstitutions(smt.d_userContext) {
+ }
Node applySubstitutions(TNode node) const {
return Rewriter::rewrite(d_topLevelSubstitutions.apply(node));
SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
d_context(em->getContext()),
- d_userContext(new Context()),
+ d_userContext(new UserContext()),
d_exprManager(em),
d_nodeManager(d_exprManager->getNodeManager()),
d_private(new smt::SmtEnginePrivate(*this)),
StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
StatisticsRegistry::registerStat(&d_staticLearningTime);
- // We have mutual dependancy here, so we add the prop engine to the theory
+ // We have mutual dependency here, so we add the prop engine to the theory
// engine later (it is non-essential there)
- d_theoryEngine = new TheoryEngine(d_context);
+ d_theoryEngine = new TheoryEngine(d_context, d_userContext);
// Add the theories
d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
throw ModalException(msg);
}
+ // Apply what was learned from preprocessing
+ Node n = d_private->applySubstitutions(e.getNode());
+
// Normalize for the theories
- Node n = theory::Rewriter::rewrite(e.getNode());
+ n = theory::Rewriter::rewrite(n);
Trace("smt") << "--- getting value of " << n << endl;
Node resultNode = d_theoryEngine->getValue(n);
namespace context {
class Context;
+ class UserContext;
}/* CVC4::context namespace */
namespace prop {
/** The context levels of user pushes */
std::vector<int> d_userLevels;
/** User level context */
- context::Context* d_userContext;
+ context::UserContext* d_userContext;
/** Our expression manager */
ExprManager* d_exprManager;
struct SlackAttrID;
typedef expr::Attribute<SlackAttrID, bool> Slack;
-TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation) :
- Theory(THEORY_ARITH, c, out, valuation),
+TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
+ Theory(THEORY_ARITH, c, u, out, valuation),
learner(d_pbSubstitutions),
d_nextIntegerCheckVar(0),
d_partialModel(c),
d_diseq(c),
d_tableau(),
d_diosolver(c, d_tableau, d_partialModel),
+ d_pbSubstitutions(u),
d_restartsCounter(0),
d_rowHasBeenAdded(false),
d_tableauResetDensity(1.6),
SimplexDecisionProcedure d_simplex;
public:
- TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation);
+ TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
virtual ~TheoryArith();
/**
using namespace CVC4::theory::arrays;
-TheoryArrays::TheoryArrays(Context* c, OutputChannel& out, Valuation valuation) :
- Theory(THEORY_ARRAY, c, out, valuation),
+TheoryArrays::TheoryArrays(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) :
+ Theory(THEORY_ARRAY, c, u, out, valuation),
d_ccChannel(this),
d_cc(c, &d_ccChannel),
d_unionFind(c),
Node recursivePreprocessTerm(TNode term);
public:
- TheoryArrays(context::Context* c, OutputChannel& out, Valuation valuation);
+ TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
~TheoryArrays();
/**
class TheoryBool : public Theory {
public:
- TheoryBool(context::Context* c, OutputChannel& out, Valuation valuation) :
- Theory(THEORY_BOOL, c, out, valuation) {
+ TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
+ Theory(THEORY_BOOL, c, u, out, valuation) {
}
Node getValue(TNode n);
class TheoryBuiltin : public Theory {
public:
- TheoryBuiltin(context::Context* c, OutputChannel& out, Valuation valuation) :
- Theory(THEORY_BUILTIN, c, out, valuation) {}
+ TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
+ Theory(THEORY_BUILTIN, c, u, out, valuation) {}
Node getValue(TNode n);
std::string identify() const { return std::string("TheoryBuiltin"); }
};/* class TheoryBuiltin */
public:
- TheoryBV(context::Context* c, OutputChannel& out, Valuation valuation)
- : Theory(THEORY_BV, c, out, valuation),
+ TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation)
+ : Theory(THEORY_BV, c, u, out, valuation),
d_eqEngine(*this, c, "theory::bv::EqualityEngine"),
d_sliceManager(*this, c),
d_context(c),
}
-TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valuation) :
- Theory(THEORY_DATATYPES, c, out, valuation),
+TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) :
+ Theory(THEORY_DATATYPES, c, u, out, valuation),
d_currAsserts(c),
d_currEqualities(c),
d_selectors(c),
CongruenceClosureExplainer<CongruenceChannel, CONGRUENCE_OPERATORS_2 (kind::APPLY_CONSTRUCTOR, kind::APPLY_SELECTOR)> d_cce;
public:
- TheoryDatatypes(context::Context* c, OutputChannel& out, Valuation valuation);
+ TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
~TheoryDatatypes();
void preRegisterTerm(TNode n);
void presolve();
using namespace CVC4::theory::uf;
using namespace CVC4::theory::uf::tim;
-TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out, Valuation valuation) :
- TheoryUF(c, out, valuation),
+TheoryUFTim::TheoryUFTim(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) :
+ Theory(THEORY_UF, c, u, out, valuation),
d_assertions(c),
d_pending(c),
d_currentPendingIdx(c,0),
namespace uf {
namespace tim {
-class TheoryUFTim : public TheoryUF {
+class TheoryUFTim : public Theory {
private:
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUFTim(context::Context* c, OutputChannel& out, Valuation valuation);
+ TheoryUFTim(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
/** Destructor for the TheoryUF object. */
~TheoryUFTim();
}
for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
Assert(substitutionCache.find(current[i]) != substitutionCache.end());
- builder << substitutionCache[current[i]];
+ builder << Node(substitutionCache[current[i]]);
}
// Mark the substitution and continue
Node result = builder;
Assert(d_substitutions.find(x) == d_substitutions.end());
// Temporary substitution cache
- NodeMap tempCache;
+ NodeMap tempCache(d_context);
tempCache[x] = t;
// Put in the new substitutions into the old ones
NodeMap::iterator it = d_substitutions.begin();
NodeMap::iterator it_end = d_substitutions.end();
for(; it != it_end; ++ it) {
- it->second = internalSubstitute(it->second, tempCache);
+ d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache);
}
// Put the new substitution in
}
}
-bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
+static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;
+static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
SubstitutionMap::NodeMap::const_iterator it = substitutions.begin();
SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end();
for (; it != it_end; ++ it) {
- if (node.hasSubterm(it->first)) {
+ if (node.hasSubterm((*it).first)) {
return false;
}
}
// Setup the cache
if (d_cacheInvalidated) {
- d_substitutionCache = d_substitutions;
+ SubstitutionMap::NodeMap::const_iterator it = d_substitutions.begin();
+ SubstitutionMap::NodeMap::const_iterator it_end = d_substitutions.end();
+ d_substitutionCache.clear();
+ for (; it != it_end; ++ it) {
+ d_substitutionCache[(*it).first] = (*it).second;
+ }
d_cacheInvalidated = false;
}
NodeMap::const_iterator it = d_substitutions.begin();
NodeMap::const_iterator it_end = d_substitutions.end();
for (; it != it_end; ++ it) {
- out << it->first << " -> " << it->second << endl;
+ out << (*it).first << " -> " << (*it).second << endl;
}
}
#include <utility>
#include <vector>
#include <algorithm>
+
#include "expr/node.h"
+#include "context/context.h"
+#include "context/cdo.h"
+#include "context/cdmap.h"
namespace CVC4 {
namespace theory {
/**
* The type for the Substitutions mapping output by
* Theory::simplify(), TheoryEngine::simplify(), and
- * Valuation::simplify(). This is in its own header to avoid circular
- * dependences between those three.
+ * Valuation::simplify(). This is in its own header to
+ * avoid circular dependences between those three.
+ *
+ * This map is context-dependent.
*/
class SubstitutionMap {
public:
- typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef context::CDMap<Node, Node, NodeHashFunction> NodeMap;
private:
+ /** The context within which this SubstitutionMap was constructed. */
+ context::Context* d_context;
+
/** The variables, in order of addition */
NodeMap d_substitutions;
NodeMap d_substitutionCache;
/** Has the cache been invalidated */
- bool d_cacheInvalidated;
+ context::CDO<bool> d_cacheInvalidated;
- /** Internaal method that performs substitution */
+ /** Internal method that performs substitution */
Node internalSubstitute(TNode t, NodeMap& substitutionCache);
public:
- SubstitutionMap(): d_cacheInvalidated(true) {}
+ SubstitutionMap(context::Context* context) :
+ d_context(context),
+ d_substitutions(context),
+ d_substitutionCache(context),
+ d_cacheInvalidated(context) {
+ }
/**
* Adds a substitution from x to t
return const_cast<SubstitutionMap*>(this)->apply(t);
}
- /**
- * Clear out the accumulated substitutions, resetting this
- * SubstitutionMap to the way it was when first constructed.
- */
- void clear() {
- d_substitutions.clear();
- d_substitutionCache.clear();
- d_cacheInvalidated = true;
- }
-
- /**
- * Swap the contents of this SubstitutionMap with those of another.
- */
- void swap(SubstitutionMap& map) {
- d_substitutions.swap(map.d_substitutions);
- d_substitutionCache.swap(map.d_substitutionCache);
- std::swap(d_cacheInvalidated, map.d_cacheInvalidated);
- }
+ // NOTE [MGD]: removed clear() and swap() from the interface
+ // when this data structure became context-dependent
+ // because they weren't used---and it's not clear how they
+ // should // best interact with cache invalidation on context
+ // pops.
/**
* Print to the output stream
*/
context::Context* d_context;
+ /**
+ * The user context for the Theory.
+ */
+ context::UserContext* d_userContext;
+
/**
* The assertFact() queue.
*
/**
* Construct a Theory.
*/
- Theory(TheoryId id, context::Context* ctxt, OutputChannel& out, Valuation valuation) throw() :
+ Theory(TheoryId id, context::Context* context, context::UserContext* userContext,
+ OutputChannel& out, Valuation valuation) throw() :
d_id(id),
- d_context(ctxt),
- d_facts(ctxt),
- d_factsHead(ctxt, 0),
- d_sharedTermsIndex(ctxt, 0),
- d_sharedTerms(ctxt),
+ d_context(context),
+ d_userContext(userContext),
+ d_facts(context),
+ d_factsHead(context, 0),
+ d_sharedTermsIndex(context, 0),
+ d_sharedTerms(context),
d_out(&out),
d_valuation(valuation)
{
return d_context;
}
+ /**
+ * Get the context associated to this Theory.
+ */
+ context::UserContext* getUserContext() const {
+ return d_userContext;
+ }
+
/**
* Set the output channel associated to this theory.
*/
using namespace CVC4;
using namespace CVC4::theory;
-TheoryEngine::TheoryEngine(context::Context* ctxt)
+TheoryEngine::TheoryEngine(context::Context* context,
+ context::UserContext* userContext)
: d_propEngine(NULL),
- d_context(ctxt),
+ d_context(context),
+ d_userContext(userContext),
d_activeTheories(0),
- d_sharedTerms(ctxt),
+ d_sharedTerms(context),
d_atomPreprocessingCache(),
d_possiblePropagations(),
- d_hasPropagated(ctxt),
- d_inConflict(ctxt, false),
+ d_hasPropagated(context),
+ d_inConflict(context, false),
d_hasShutDown(false),
- d_incomplete(ctxt, false),
- d_sharedAssertions(ctxt),
+ d_incomplete(context, false),
+ d_sharedAssertions(context),
d_logic(""),
- d_propagatedLiterals(ctxt),
- d_propagatedLiteralsIndex(ctxt, 0),
- d_preRegistrationVisitor(this, ctxt),
+ d_propagatedLiterals(context),
+ d_propagatedLiteralsIndex(context, 0),
+ d_preRegistrationVisitor(this, context),
d_sharedTermsVisitor(d_sharedTerms)
{
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
theory::Rewriter::shutdown();
}
-theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) {
+theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
Trace("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
- Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitionOut);
+ Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitutionOut);
Trace("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
return solveStatus;
}
/** Our context */
context::Context* d_context;
+ /** Our user context */
+ context::UserContext* d_userContext;
+
/**
* A table of from theory IDs to theory pointers. Never use this table
* directly, use theoryOf() instead.
public:
/** Constructs a theory engine */
- TheoryEngine(context::Context* ctxt);
+ TheoryEngine(context::Context* context, context::UserContext* userContext);
/** Destroys a theory engine */
~TheoryEngine();
inline void addTheory(theory::TheoryId theoryId) {
Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId);
- d_theoryTable[theoryId] = new TheoryClass(d_context, *d_theoryOut[theoryId], theory::Valuation(this));
+ d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this));
}
/**
/**
* Solve the given literal with a theory that owns it.
*/
- theory::Theory::SolveStatus solve(TNode literal, theory::SubstitutionMap& substitionOut);
+ theory::Theory::SolveStatus solve(TNode literal,
+ theory::SubstitutionMap& substitutionOut);
/**
* Preregister a Theory atom with the responsible theory (or
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation):
- Theory(THEORY_UF, ctxt, out, valuation),
+ TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation):
+ Theory(THEORY_UF, c, u, out, valuation),
d_notify(*this),
- d_equalityEngine(d_notify, ctxt, "theory::uf::TheoryUF"),
- d_knownFacts(ctxt),
- d_conflict(ctxt, false),
- d_literalsToPropagate(ctxt),
- d_literalsToPropagateIndex(ctxt, 0)
+ d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"),
+ d_knownFacts(c),
+ d_conflict(c, false),
+ d_literalsToPropagate(c),
+ d_literalsToPropagateIndex(c, 0)
{
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::APPLY_UF);
/** The context */
Context* d_context;
+ /** The user context */
+ UserContext* d_userContext;
+
/** The node manager */
NodeManager* d_nodeManager;
-void setUp() {
- d_context = new Context;
- d_nodeManager = new NodeManager(d_context, NULL);
- NodeManagerScope nms(d_nodeManager);
- d_satSolver = new FakeSatSolver;
- d_theoryEngine = new TheoryEngine(d_context);
- d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
- d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL);
- d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH);
- theory::Registrar registrar(d_theoryEngine);
- d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar);
-}
-
-void tearDown() {
- NodeManagerScope nms(d_nodeManager);
- delete d_cnfStream;
- d_theoryEngine->shutdown();
- delete d_theoryEngine;
- delete d_satSolver;
- delete d_nodeManager;
- delete d_context;
-}
+ void setUp() {
+ d_context = new Context();
+ d_userContext = new UserContext();
+ d_nodeManager = new NodeManager(d_context, NULL);
+ NodeManagerScope nms(d_nodeManager);
+ d_satSolver = new FakeSatSolver();
+ d_theoryEngine = new TheoryEngine(d_context, d_userContext);
+ d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
+ d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL);
+ d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH);
+ theory::Registrar registrar(d_theoryEngine);
+ d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar);
+ }
+
+ void tearDown() {
+ NodeManagerScope nms(d_nodeManager);
+ delete d_cnfStream;
+ d_theoryEngine->shutdown();
+ delete d_theoryEngine;
+ delete d_satSolver;
+ delete d_nodeManager;
+ delete d_userContext;
+ delete d_context;
+ }
public:
-/* [chris 5/26/2010] In the tests below, we don't attempt to delve into the
- * deep structure of the CNF conversion. Firstly, we just want to make sure
- * that the conversion doesn't choke on any boolean Exprs. We'll also check
- * that addClause got called. We won't check that it gets called a particular
- * number of times, or with what.
- */
-
-void testAnd() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testComplexExpr() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(
- kind::IMPLIES,
- d_nodeManager->mkNode(kind::AND, a, b),
- d_nodeManager->mkNode(
- kind::IFF,
- d_nodeManager->mkNode(kind::OR, c, d),
- d_nodeManager->mkNode(
- kind::NOT,
- d_nodeManager->mkNode(kind::XOR, e, f)))), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testFalse() {
- NodeManagerScope nms(d_nodeManager);
- d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testIff() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::IFF, a, b), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testImplies() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-// ITEs should be removed before going to CNF
-//void testIte() {
-// NodeManagerScope nms(d_nodeManager);
-// d_cnfStream->convertAndAssert(
-// d_nodeManager->mkNode(
-// kind::EQUAL,
-// d_nodeManager->mkNode(
-// kind::ITE,
-// d_nodeManager->mkVar(d_nodeManager->booleanType()),
-// d_nodeManager->mkVar(d_nodeManager->integerType()),
-// d_nodeManager->mkVar(d_nodeManager->integerType())
-// ),
-// d_nodeManager->mkVar(d_nodeManager->integerType())
-// ), false, false);
-//
-//}
-
-void testNot() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::NOT, a), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testOr() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::OR, a, b, c), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testTrue() {
- NodeManagerScope nms(d_nodeManager);
- d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testVar() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(a, false, false);
- TS_ASSERT( d_satSolver->addClauseCalled() );
- d_satSolver->reset();
- d_cnfStream->convertAndAssert(b, false, false);
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testXor() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::XOR, a, b), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
+ /* [chris 5/26/2010] In the tests below, we don't attempt to delve into the
+ * deep structure of the CNF conversion. Firstly, we just want to make sure
+ * that the conversion doesn't choke on any boolean Exprs. We'll also check
+ * that addClause got called. We won't check that it gets called a particular
+ * number of times, or with what.
+ */
+
+ void testAnd() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testComplexExpr() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(
+ kind::IMPLIES,
+ d_nodeManager->mkNode(kind::AND, a, b),
+ d_nodeManager->mkNode(
+ kind::IFF,
+ d_nodeManager->mkNode(kind::OR, c, d),
+ d_nodeManager->mkNode(
+ kind::NOT,
+ d_nodeManager->mkNode(kind::XOR, e, f)))), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testFalse() {
+ NodeManagerScope nms(d_nodeManager);
+ d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testIff() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::IFF, a, b), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testImplies() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ // ITEs should be removed before going to CNF
+ //void testIte() {
+ // NodeManagerScope nms(d_nodeManager);
+ // d_cnfStream->convertAndAssert(
+ // d_nodeManager->mkNode(
+ // kind::EQUAL,
+ // d_nodeManager->mkNode(
+ // kind::ITE,
+ // d_nodeManager->mkVar(d_nodeManager->booleanType()),
+ // d_nodeManager->mkVar(d_nodeManager->integerType()),
+ // d_nodeManager->mkVar(d_nodeManager->integerType())
+ // ),
+ // d_nodeManager->mkVar(d_nodeManager->integerType())
+ // ), false, false);
+ //
+ //}
+
+ void testNot() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::NOT, a), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testOr() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::OR, a, b, c), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testTrue() {
+ NodeManagerScope nms(d_nodeManager);
+ d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testVar() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(a, false, false);
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ d_satSolver->reset();
+ d_cnfStream->convertAndAssert(b, false, false);
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testXor() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::XOR, a, b), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
};
class TheoryArithWhite : public CxxTest::TestSuite {
Context* d_ctxt;
+ UserContext* d_uctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
}
void setUp() {
- d_ctxt = new Context;
+ d_ctxt = new Context();
+ d_uctxt = new UserContext();
d_nm = new NodeManager(d_ctxt, NULL);
d_scope = new NodeManagerScope(d_nm);
d_outputChannel.clear();
- d_arith = new TheoryArith(d_ctxt, d_outputChannel, Valuation(NULL));
+ d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL));
preregistered = new std::set<Node>();
d_outputChannel.clear();
delete d_scope;
delete d_nm;
+ delete d_uctxt;
delete d_ctxt;
}
set<Node> d_registered;
vector<Node> d_getSequence;
- DummyTheory(Context* ctxt, OutputChannel& out, Valuation valuation) :
- Theory(theory::THEORY_BUILTIN, ctxt, out, valuation) {
+ DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation) :
+ Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation) {
}
void registerTerm(TNode n) {
void explain(TNode n, Effort level) {}
Node getValue(TNode n) { return Node::null(); }
string identify() const { return "DummyTheory"; }
-};
+};/* class DummyTheory */
class TheoryBlack : public CxxTest::TestSuite {
Context* d_ctxt;
+ UserContext* d_uctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
public:
void setUp() {
- d_ctxt = new Context;
+ d_ctxt = new Context();
+ d_uctxt = new UserContext();
d_nm = new NodeManager(d_ctxt, NULL);
d_scope = new NodeManagerScope(d_nm);
- d_dummy = new DummyTheory(d_ctxt, d_outputChannel, Valuation(NULL));
+ d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL));
d_outputChannel.clear();
atom0 = d_nm->mkConst(true);
atom1 = d_nm->mkConst(false);
delete d_dummy;
delete d_scope;
delete d_nm;
+ delete d_uctxt;
delete d_ctxt;
}
// static std::deque<RewriteItem> s_expected;
public:
- FakeTheory(context::Context* ctxt, OutputChannel& out, Valuation valuation) :
- Theory(theoryId, ctxt, out, valuation)
+ FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation) :
+ Theory(theoryId, ctxt, uctxt, out, valuation)
{ }
/** Register an expected rewrite call */
*/
class TheoryEngineWhite : public CxxTest::TestSuite {
Context* d_ctxt;
+ UserContext* d_uctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
public:
void setUp() {
- d_ctxt = new Context;
+ d_ctxt = new Context();
+ d_uctxt = new UserContext();
d_nm = new NodeManager(d_ctxt, NULL);
d_scope = new NodeManagerScope(d_nm);
- d_nullChannel = new FakeOutputChannel;
+ d_nullChannel = new FakeOutputChannel();
// create the TheoryEngine
- d_theoryEngine = new TheoryEngine(d_ctxt);
+ d_theoryEngine = new TheoryEngine(d_ctxt, d_uctxt);
d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN);
d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL);
delete d_scope;
delete d_nm;
+ delete d_uctxt;
delete d_ctxt;
}
projects / cvc5.git / commitdiff