stringstream statName; \
statName << "expr::ExprManager::" << kind; \
d_exprStatistics[kind] = new IntStat(statName.str(), 0); \
- StatisticsRegistry::registerStat(d_exprStatistics[kind]); \
+ d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatistics[kind]); \
} \
++ *(d_exprStatistics[kind]); \
}
statName << "expr::ExprManager::VARIABLE:" << type; \
} \
d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \
- StatisticsRegistry::registerStat(d_exprStatisticsVars[type]); \
+ d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \
} \
++ *(d_exprStatisticsVars[type]); \
}
for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
d_exprStatistics[i] = NULL;
}
- for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
+ for (unsigned i = 0; i < LAST_TYPE; ++ i) {
d_exprStatisticsVars[i] = NULL;
}
#endif
d_ctxt(new Context()),
d_nodeManager(new NodeManager(d_ctxt, this, options)) {
#ifdef CVC4_STATISTICS_ON
- for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
+ for (unsigned i = 0; i < LAST_TYPE; ++ i) {
d_exprStatisticsVars[i] = NULL;
}
for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
#ifdef CVC4_STATISTICS_ON
for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
if (d_exprStatistics[i] != NULL) {
- StatisticsRegistry::unregisterStat(d_exprStatistics[i]);
+ d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatistics[i]);
delete d_exprStatistics[i];
}
}
- for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
+ for (unsigned i = 0; i < LAST_TYPE; ++ i) {
if (d_exprStatisticsVars[i] != NULL) {
- StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]);
+ d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatisticsVars[i]);
delete d_exprStatisticsVars[i];
}
}
return d_ctxt;
}
+StatisticsRegistry* ExprManager::getStatisticsRegistry() const throw() {
+ return d_nodeManager->getStatisticsRegistry();
+}
+
namespace expr {
Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
#include "expr/type.h"
#include "expr/expr.h"
#include "util/subrange_bound.h"
+#include "util/stats.h"
${includes}
// compiler directs the user to the template file instead of the
// generated one. We don't want the user to modify the generated one,
// since it'll get overwritten on a later build.
-#line 38 "${template}"
+#line 39 "${template}"
namespace CVC4 {
NodeManager* d_nodeManager;
/** Counts of expressions and variables created of a given kind */
- IntStat* d_exprStatisticsVars[LAST_TYPE + 1];
+ IntStat* d_exprStatisticsVars[LAST_TYPE];
IntStat* d_exprStatistics[kind::LAST_KIND];
/**
Expr mkVar(const std::string& name, Type type);
Expr mkVar(Type type);
+ /** Get a reference to the statistics registry for this ExprManager */
+ StatisticsRegistry* getStatisticsRegistry() const throw();
+
/** Export an expr to a different ExprManager */
//static Expr exportExpr(const Expr& e, ExprManager* em);
/** Export a type to a different ExprManager */
}
/** Get this node manager's statistics registry */
- StatisticsRegistry* getStatisticsRegistry() const {
+ StatisticsRegistry* getStatisticsRegistry() const throw() {
return d_statisticsRegistry;
}
Debug("current") << "node manager scope: "
<< "returning to " << NodeManager::s_current << "\n";
}
-};
+};/* class NodeManagerScope */
template <class AttrKind>
// signal handlers need access
pStatistics = smt.getStatisticsRegistry();
+ pStatistics->registerStat_(exprMgr.getStatisticsRegistry());
// Timer statistic
RegisterStatistic statTotalTime(exprMgr, &s_totalTime);
theStatisticsRegistry.registerStat_((&driverStatisticsRegistry));
// Timer statistic
- RegisterStatistic* statTotatTime =
+ RegisterStatistic* statTotalTime =
new RegisterStatistic(&driverStatisticsRegistry, &s_totalTime);
RegisterStatistic* statBeforePortfolioTime =
new RegisterStatistic(&driverStatisticsRegistry, &s_beforePortfolioTime);
// Register the statistics registry of the thread
string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id);
smts[i]->getStatisticsRegistry()->setName(tag);
- theStatisticsRegistry.registerStat_( (Stat*)smts[i]->getStatisticsRegistry() );
+ theStatisticsRegistry.registerStat_( smts[i]->getStatisticsRegistry() );
+ theStatisticsRegistry.registerStat_( exprMgrs[i]->getStatisticsRegistry() );
}
/************************* Lemma sharing init ************************/
//delete vmaps;
- delete statTotatTime;
+ delete statTotalTime;
delete statBeforePortfolioTime;
delete statFilenameReg;
libsmt_la_SOURCES = \
smt_engine.cpp \
smt_engine.h \
+ smt_engine_scope.cpp \
+ smt_engine_scope.h \
modal_exception.h \
bad_option_exception.h \
no_such_function_exception.h
#include "smt/modal_exception.h"
#include "smt/no_such_function_exception.h"
#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "theory/theory_engine.h"
#include "proof/proof_manager.h"
#include "util/proof.h"
#include "util/output.h"
#include "util/hash.h"
#include "theory/substitutions.h"
-#include "theory/builtin/theory_builtin.h"
-#include "theory/booleans/theory_bool.h"
-#include "theory/booleans/circuit_propagator.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/arrays/theory_arrays.h"
-#include "theory/bv/theory_bv.h"
-#include "theory/datatypes/theory_datatypes.h"
#include "theory/theory_traits.h"
#include "theory/logic_info.h"
+#include "theory/booleans/circuit_propagator.h"
#include "util/ite_removal.h"
#include "theory/model.h"
d_cumulativeResourceUsed(0),
d_status(),
d_private(new smt::SmtEnginePrivate(*this)),
+ d_statisticsRegistry(new StatisticsRegistry()),
d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
StatisticsRegistry::registerStat(&d_definitionExpansionTime);
StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
}
SmtEngine::~SmtEngine() throw() {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
try {
while(Options::current()->incrementalSolving && d_userContext->getLevel() > 1) {
delete d_theoryEngine;
delete d_propEngine;
//delete d_decisionEngine;
+
+ delete d_statisticsRegistry;
+
} catch(Exception& e) {
Warning() << "CVC4 threw an exception during cleanup." << endl
<< e << endl;
}
void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
if(Dump.isOn("benchmark")) {
Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
}
void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
setLogic(LogicInfo(s));
}
void SmtEngine::setInfo(const std::string& key, const SExpr& value)
throw(BadOptionException, ModalException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
if(Dump.isOn("benchmark")) {
if(! value.isAtom()) {
throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string");
}
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
d_logic = value.getValue();
setLogicInternal();
return;
SExpr SmtEngine::getInfo(const std::string& key) const
throw(BadOptionException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
Trace("smt") << "SMT getInfo(" << key << ")" << endl;
if(key == ":all-statistics") {
void SmtEngine::setOption(const std::string& key, const SExpr& value)
throw(BadOptionException, ModalException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
if(Dump.isOn("benchmark")) {
SExpr SmtEngine::getOption(const std::string& key) const
throw(BadOptionException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
Trace("smt") << "SMT getOption(" << key << ")" << endl;
if(Dump.isOn("benchmark")) {
<< func;
Dump("declarations") << DefineFunctionCommand(ss.str(), func, formals, formula);
}
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
// type check body
Type formulaType = formula.getType(Options::current()->typeChecking);
Assert(e.isNull() || e.getExprManager() == d_exprManager);
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
Assert(!e.isNull());
Assert(e.getExprManager() == d_exprManager);
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
Result SmtEngine::assertFormula(const BoolExpr& e) {
Assert(e.getExprManager() == d_exprManager);
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
Trace("smt") << "SmtEngine::assertFormula(" << e << ")" << endl;
ensureBoolean(e);
Expr SmtEngine::simplify(const Expr& e) {
Assert(e.getExprManager() == d_exprManager);
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
if( Options::current()->typeChecking ) {
e.getType(true);// ensure expr is type-checked at this point
Expr SmtEngine::getValue(const Expr& e)
throw(ModalException, AssertionException) {
Assert(e.getExprManager() == d_exprManager);
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
// ensure expr is type-checked at this point
Type type = e.getType(Options::current()->typeChecking);
}
bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
Type type = e.getType(Options::current()->typeChecking);
// must be Boolean
SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
Trace("smt") << "SMT getAssignment()" << endl;
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetAssignmentCommand();
void SmtEngine::addToModelType( Type& t ){
Trace("smt") << "SMT addToModelType(" << t << ")" << endl;
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
if( Options::current()->produceModels ) {
d_theoryEngine->getModel()->addDefineType( TypeNode::fromType( t ) );
}
void SmtEngine::addToModelFunction( Expr& e ){
Trace("smt") << "SMT addToModelFunction(" << e << ")" << endl;
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
if( Options::current()->produceModels ) {
d_theoryEngine->getModel()->addDefineFunction( e.getNode() );
}
Model* SmtEngine::getModel() throw(ModalException, AssertionException){
Trace("smt") << "SMT getModel()" << endl;
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
if(!Options::current()->produceModels) {
const char* msg =
Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
Trace("smt") << "SMT getProof()" << endl;
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetProofCommand();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetAssertionsCommand();
}
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
Trace("smt") << "SMT getAssertions()" << endl;
if(!Options::current()->interactive) {
const char* msg =
}
size_t SmtEngine::getStackLevel() const {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
Trace("smt") << "SMT getStackLevel()" << endl;
return d_context->getLevel();
}
void SmtEngine::push() {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
Trace("smt") << "SMT push()" << endl;
d_private->processAssertions();
}
void SmtEngine::pop() {
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
finalOptionsAreSet();
Trace("smt") << "SMT pop()" << endl;
if(Dump.isOn("benchmark")) {
}
StatisticsRegistry* SmtEngine::getStatisticsRegistry() const {
- return d_exprManager->d_nodeManager->getStatisticsRegistry();
+ return d_statisticsRegistry;
}
void SmtEngine::printModel( std::ostream& out, Model* m ){
- NodeManagerScope nms(d_nodeManager);
+ SmtScope smts(this);
m->toStream(out);
}
class DefinedFunction;
class SmtEnginePrivate;
+ class SmtScope;
}/* CVC4::smt namespace */
// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
void setLogicInternal() throw(AssertionException);
friend class ::CVC4::smt::SmtEnginePrivate;
+ friend class ::CVC4::smt::SmtScope;
+
+ StatisticsRegistry* d_statisticsRegistry;
// === STATISTICS ===
/** time spent in definition-expansion */
--- /dev/null
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+
+namespace CVC4 {
+namespace smt {
+
+CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current = NULL;
+
+}
+}
--- /dev/null
+#include "smt/smt_engine.h"
+#include "util/tls.h"
+#include "util/Assert.h"
+#include "expr/node_manager.h"
+#include "util/output.h"
+
+#pragma once
+
+namespace CVC4 {
+namespace smt {
+
+extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current;
+
+inline SmtEngine* currentSmtEngine() {
+ Assert(s_smtEngine_current != NULL);
+ return s_smtEngine_current;
+}
+
+class SmtScope : public NodeManagerScope {
+ /** The old NodeManager, to be restored on destruction. */
+ SmtEngine* d_oldSmtEngine;
+
+public:
+
+ SmtScope(const SmtEngine* smt) :
+ NodeManagerScope(smt->d_nodeManager),
+ d_oldSmtEngine(s_smtEngine_current) {
+ Assert(smt != NULL);
+ s_smtEngine_current = const_cast<SmtEngine*>(smt);
+ Debug("current") << "smt scope: " << s_smtEngine_current << std::endl;
+ }
+
+ ~SmtScope() {
+ s_smtEngine_current = d_oldSmtEngine;
+ Debug("current") << "smt scope: returning to " << s_smtEngine_current << std::endl;
+ }
+};/* class SmtScope */
+
+}
+}
#include "util/stats.h"
#include "expr/node_manager.h"
#include "expr/expr_manager_scope.h"
+#include "expr/expr_manager.h"
#include "lib/clock_gettime.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/smt_engine.h"
#ifdef CVC4_STATISTICS_ON
# define __CVC4_USE_STATISTICS true
std::string StatisticsRegistry::s_regDelim("::");
StatisticsRegistry* StatisticsRegistry::current() {
- return NodeManager::currentNM()->getStatisticsRegistry();
+ return smt::currentSmtEngine()->getStatisticsRegistry();
}
void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
#ifdef CVC4_STATISTICS_ON
- StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats;
+ StatSet& registeredStats = current()->d_registeredStats;
AlwaysAssert(registeredStats.find(s) == registeredStats.end(),
"Statistic `%s' was already registered with this registry.", s->getName().c_str());
registeredStats.insert(s);
void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
#ifdef CVC4_STATISTICS_ON
- StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats;
+ StatSet& registeredStats = current()->d_registeredStats;
AlwaysAssert(registeredStats.find(s) != registeredStats.end(),
"Statistic `%s' was not registered with this registry.", s->getName().c_str());
registeredStats.erase(s);
}
StatisticsRegistry::const_iterator StatisticsRegistry::begin() {
- return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin();
+ return current()->d_registeredStats.begin();
}/* StatisticsRegistry::begin() */
StatisticsRegistry::const_iterator StatisticsRegistry::end() {
- return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.end();
+ return current()->d_registeredStats.end();
}/* StatisticsRegistry::end() */
void TimerStat::start() {
}/* TimerStat::stop() */
RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
- d_reg(NULL),
+ d_reg(em.getStatisticsRegistry()),
d_stat(stat) {
- ExprManagerScope ems(em);
- d_reg = StatisticsRegistry::current();
d_reg->registerStat_(d_stat);
}
+
+RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) :
+ d_reg(smt.getStatisticsRegistry()),
+ d_stat(stat) {
+ d_reg->registerStat_(d_stat);
+}
+
#endif
class ExprManager;
+class SmtEngine;
class CVC4_PUBLIC Stat;
RegisterStatistic(ExprManager& em, Stat* stat);
+ RegisterStatistic(SmtEngine& smt, Stat* stat);
+
~RegisterStatistic() {
d_reg->unregisterStat_(d_stat);
}
TEST_EXTENSIONS = .class
CPLUSPLUS_TESTS = \
boilerplate \
- ouroborous
+ ouroborous \
+ two_smt_engines
# cvc3_main
TESTS = $(CPLUSPLUS_TESTS)
int main() {
ExprManager em;
Options opts;
+ cout << "foo: " << opts.threadArgv.size() << endl;
SmtEngine smt(&em);
Result r = smt.query(em.mkConst(true));
--- /dev/null
+/********************* */
+/*! \file two_smt_engines.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A simple test of multiple SmtEngines
+ **
+ ** A simple test of multiple SmtEngines.
+ **/
+
+#include <iostream>
+#include <sstream>
+
+#include "expr/expr.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4;
+using namespace std;
+
+int main() {
+ ExprManager em;
+ Options opts;
+ SmtEngine smt(&em);
+ SmtEngine smt2(&em);
+ Result r = smt.query(em.mkConst(true));
+
+ return r == Result::VALID ? 0 : 1;
+}
+
UNIT_TESTS = \
theory/logic_info_white \
theory/theory_engine_white \
- theory/theory_black \
+ theory/theory_white \
theory/theory_arith_white \
theory/union_find_black \
theory/theory_bv_white \
expr/type_node_white \
parser/parser_black \
parser/parser_builder_black \
- prop/cnf_stream_black \
+ prop/cnf_stream_white \
context/context_black \
context/context_white \
context/context_mm_black \
+++ /dev/null
-/********************* */
-/*! \file cnf_stream_black.h
- ** \verbatim
- ** Original author: cconway
- ** Major contributors: mdeters
- ** Minor contributors (to current version): taking, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief White box testing of CVC4::prop::CnfStream.
- **
- ** White box testing of CVC4::prop::CnfStream.
- **/
-
-#include <cxxtest/TestSuite.h>
-/* #include <gmock/gmock.h> */
-/* #include <gtest/gtest.h> */
-
-#include "util/Assert.h"
-
-
-#include "expr/expr_manager.h"
-#include "expr/node_manager.h"
-#include "context/context.h"
-#include "prop/cnf_stream.h"
-#include "prop/prop_engine.h"
-#include "prop/theory_proxy.h"
-#include "smt/smt_engine.h"
-
-#include "theory/theory.h"
-#include "theory/theory_engine.h"
-#include "theory/theory_registrar.h"
-
-#include "theory/builtin/theory_builtin.h"
-#include "theory/booleans/theory_bool.h"
-#include "theory/arith/theory_arith.h"
-
-using namespace CVC4;
-using namespace CVC4::context;
-using namespace CVC4::prop;
-using namespace std;
-
-/* This fake class relies on the face that a MiniSat variable is just an int. */
-class FakeSatSolver : public SatSolver {
- SatVariable d_nextVar;
- bool d_addClauseCalled;
-
-public:
- FakeSatSolver() :
- d_nextVar(0),
- d_addClauseCalled(false) {
- }
-
- SatVariable newVar(bool theoryAtom) {
- return d_nextVar++;
- }
-
- SatVariable trueVar() {
- return d_nextVar++;
- }
-
- SatVariable falseVar() {
- return d_nextVar++;
- }
-
- void addClause(SatClause& c, bool lemma) {
- d_addClauseCalled = true;
- }
-
- void reset() {
- d_addClauseCalled = false;
- }
-
- unsigned int addClauseCalled() {
- return d_addClauseCalled;
- }
-
- unsigned getAssertionLevel() const {
- return 0;
- }
-
- bool isDecision(Node) const {
- return false;
- }
-
- void unregisterVar(SatLiteral lit) {
- }
-
- void renewVar(SatLiteral lit, int level = -1) {
- }
-
- void interrupt() {
- }
-
- SatValue solve() {
- return SAT_VALUE_UNKNOWN;
- }
-
- SatValue solve(long unsigned int& resource) {
- return SAT_VALUE_UNKNOWN;
- }
-
- SatValue value(SatLiteral l) {
- return SAT_VALUE_UNKNOWN;
- }
-
- SatValue modelValue(SatLiteral l) {
- return SAT_VALUE_UNKNOWN;
- }
-
- bool properExplanation(SatLiteral lit, SatLiteral expl) const {
- return true;
- }
-
-};/* class FakeSatSolver */
-
-class CnfStreamBlack : public CxxTest::TestSuite {
- /** The SAT solver proxy */
- FakeSatSolver* d_satSolver;
-
- /** The logic info */
- LogicInfo* d_logicInfo;
-
- /** The theory engine */
- TheoryEngine* d_theoryEngine;
-
- /** The output channel */
- theory::OutputChannel* d_outputChannel;
-
- /** The CNF converter in use */
- CnfStream* d_cnfStream;
-
- /** The context */
- Context* d_context;
-
- /** The user context */
- UserContext* d_userContext;
-
- /** The node manager */
- NodeManager* d_nodeManager;
-
- 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_logicInfo = new LogicInfo();
- d_logicInfo->lock();
- d_theoryEngine = new TheoryEngine(d_context, d_userContext, *d_logicInfo);
- 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);
- d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine));
- }
-
- void tearDown() {
- NodeManagerScope nms(d_nodeManager);
- delete d_cnfStream;
- d_theoryEngine->shutdown();
- delete d_theoryEngine;
- delete d_logicInfo;
- 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 testTrue() {
- NodeManagerScope nms(d_nodeManager);
- d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), 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 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() );
- }
-
- void testEnsureLiteral() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
- d_cnfStream->ensureLiteral(a_and_b);
- // Clauses are necessary to "literal-ize" a_and_b; this perhaps
- // doesn't belong in a black-box test though...
- TS_ASSERT( d_satSolver->addClauseCalled() );
- TS_ASSERT( d_cnfStream->hasLiteral(a_and_b) );
- }
-};
--- /dev/null
+/********************* */
+/*! \file cnf_stream_white.h
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): taking, dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief White box testing of CVC4::prop::CnfStream.
+ **
+ ** White box testing of CVC4::prop::CnfStream.
+ **/
+
+#include <cxxtest/TestSuite.h>
+/* #include <gmock/gmock.h> */
+/* #include <gtest/gtest.h> */
+
+#include "util/Assert.h"
+
+#include "expr/expr_manager.h"
+#include "expr/node_manager.h"
+#include "context/context.h"
+#include "prop/cnf_stream.h"
+#include "prop/prop_engine.h"
+#include "prop/theory_proxy.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
+#include "theory/theory_registrar.h"
+
+#include "theory/builtin/theory_builtin.h"
+#include "theory/booleans/theory_bool.h"
+#include "theory/arith/theory_arith.h"
+
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace CVC4::prop;
+using namespace CVC4::smt;
+using namespace CVC4::theory;
+using namespace std;
+
+/* This fake class relies on the face that a MiniSat variable is just an int. */
+class FakeSatSolver : public SatSolver {
+ SatVariable d_nextVar;
+ bool d_addClauseCalled;
+
+public:
+ FakeSatSolver() :
+ d_nextVar(0),
+ d_addClauseCalled(false) {
+ }
+
+ SatVariable newVar(bool theoryAtom) {
+ return d_nextVar++;
+ }
+
+ SatVariable trueVar() {
+ return d_nextVar++;
+ }
+
+ SatVariable falseVar() {
+ return d_nextVar++;
+ }
+
+ void addClause(SatClause& c, bool lemma) {
+ d_addClauseCalled = true;
+ }
+
+ void reset() {
+ d_addClauseCalled = false;
+ }
+
+ unsigned int addClauseCalled() {
+ return d_addClauseCalled;
+ }
+
+ unsigned getAssertionLevel() const {
+ return 0;
+ }
+
+ bool isDecision(Node) const {
+ return false;
+ }
+
+ void unregisterVar(SatLiteral lit) {
+ }
+
+ void renewVar(SatLiteral lit, int level = -1) {
+ }
+
+ void interrupt() {
+ }
+
+ SatValue solve() {
+ return SAT_VALUE_UNKNOWN;
+ }
+
+ SatValue solve(long unsigned int& resource) {
+ return SAT_VALUE_UNKNOWN;
+ }
+
+ SatValue value(SatLiteral l) {
+ return SAT_VALUE_UNKNOWN;
+ }
+
+ SatValue modelValue(SatLiteral l) {
+ return SAT_VALUE_UNKNOWN;
+ }
+
+ bool properExplanation(SatLiteral lit, SatLiteral expl) const {
+ return true;
+ }
+
+};/* class FakeSatSolver */
+
+class CnfStreamWhite : public CxxTest::TestSuite {
+ /** The SAT solver proxy */
+ FakeSatSolver* d_satSolver;
+
+ /** The theory engine */
+ TheoryEngine* d_theoryEngine;
+
+ /** The CNF converter in use */
+ CnfStream* d_cnfStream;
+
+ /** The context */
+ Context* d_context;
+
+ /** The user context */
+ UserContext* d_userContext;
+
+ /** The node manager */
+ NodeManager* d_nodeManager;
+
+ ExprManager* d_exprManager;
+ SmtScope* d_scope;
+ SmtEngine* d_smt;
+
+ void setUp() {
+ d_exprManager = new ExprManager();
+ d_smt = new SmtEngine(d_exprManager);
+ d_smt->d_logic.lock();
+ d_nodeManager = NodeManager::fromExprManager(d_exprManager);
+ d_scope = new SmtScope(d_smt);
+
+ d_context = d_smt->d_context;
+ d_userContext = d_smt->d_userContext;
+
+ d_theoryEngine = d_smt->d_theoryEngine;
+
+ d_satSolver = new FakeSatSolver();
+ d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine));
+ }
+
+ void tearDown() {
+ delete d_cnfStream;
+ delete d_satSolver;
+ delete d_scope;
+ delete d_smt;
+ delete d_exprManager;
+ }
+
+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 testTrue() {
+ NodeManagerScope nms(d_nodeManager);
+ d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), 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 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() );
+ }
+
+ void testEnsureLiteral() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
+ d_cnfStream->ensureLiteral(a_and_b);
+ // Clauses are necessary to "literal-ize" a_and_b
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ TS_ASSERT( d_cnfStream->hasLiteral(a_and_b) );
+ }
+};
#include <cxxtest/TestSuite.h>
#include "theory/theory.h"
+#include "theory/theory_engine.h"
#include "theory/arith/theory_arith.h"
#include "theory/quantifiers_engine.h"
#include "expr/node.h"
#include "expr/node_manager.h"
#include "context/context.h"
#include "util/rational.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "theory/theory_test_utils.h"
using namespace CVC4::expr;
using namespace CVC4::context;
using namespace CVC4::kind;
+using namespace CVC4::smt;
using namespace std;
Context* d_ctxt;
UserContext* d_uctxt;
+ ExprManager* d_em;
NodeManager* d_nm;
- NodeManagerScope* d_scope;
+ SmtScope* d_scope;
+ SmtEngine* d_smt;
TestOutputChannel d_outputChannel;
LogicInfo d_logicInfo;
Theory::Effort d_level;
- QuantifiersEngine* d_quantifiersEngine;
TheoryArith* d_arith;
TypeNode* d_booleanType;
}
void setUp() {
- d_ctxt = new Context();
- d_uctxt = new UserContext();
- d_nm = new NodeManager(d_ctxt, NULL);
- d_scope = new NodeManagerScope(d_nm);
+ d_em = new ExprManager();
+ d_nm = NodeManager::fromExprManager(d_em);
+ d_smt = new SmtEngine(d_em);
+ d_ctxt = d_smt->d_context;
+ d_uctxt = d_smt->d_userContext;
+ d_scope = new SmtScope(d_smt);
d_outputChannel.clear();
d_logicInfo.lock();
- d_quantifiersEngine = new QuantifiersEngine(d_ctxt, NULL);
- d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo, d_quantifiersEngine);
+
+ // guard against duplicate statistics assertion errors
+ delete d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH];
+ delete d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH];
+ d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH] = NULL;
+ d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH] = NULL;
+
+ d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo, d_smt->d_theoryEngine->d_quantEngine);
preregistered = new std::set<Node>();
delete preregistered;
delete d_arith;
- delete d_quantifiersEngine;
d_outputChannel.clear();
delete d_scope;
- delete d_nm;
- delete d_uctxt;
- delete d_ctxt;
+ delete d_smt;
+ delete d_em;
}
void testAssert() {
+++ /dev/null
-/********************* */
-/*! \file theory_black.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: barrett, mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Black box testing of CVC4::theory::Theory.
- **
- ** Black box testing of CVC4::theory::Theory.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "theory/theory.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "context/context.h"
-
-#include <vector>
-
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::expr;
-using namespace CVC4::context;
-
-using namespace std;
-
-/**
- * Very basic OutputChannel for testing simple Theory Behaviour.
- * Stores a call sequence for the output channel
- */
-enum OutputChannelCallType{CONFLICT, PROPAGATE, LEMMA, EXPLANATION};
-class TestOutputChannel : public OutputChannel {
-private:
- void push(OutputChannelCallType call, TNode n) {
- d_callHistory.push_back(make_pair(call, n));
- }
-
-public:
- vector< pair<OutputChannelCallType, Node> > d_callHistory;
-
- TestOutputChannel() {}
-
- ~TestOutputChannel() {}
-
- void safePoint() throw(Interrupted, AssertionException) {}
-
- void conflict(TNode n)
- throw(AssertionException) {
- push(CONFLICT, n);
- }
-
- bool propagate(TNode n)
- throw(AssertionException) {
- push(PROPAGATE, n);
- return true;
- }
-
- void propagateAsDecision(TNode n)
- throw(AssertionException) {
- // ignore
- }
-
- LemmaStatus lemma(TNode n, bool removable)
- throw(AssertionException) {
- push(LEMMA, n);
- return LemmaStatus(Node::null(), 0);
- }
-
- void requirePhase(TNode, bool)
- throw(Interrupted, AssertionException) {
- Unreachable();
- }
-
- bool flipDecision()
- throw(Interrupted, AssertionException) {
- Unreachable();
- }
-
- void setIncomplete()
- throw(AssertionException) {
- Unreachable();
- }
-
- void clear() {
- d_callHistory.clear();
- }
-
- Node getIthNode(int i) {
- Node tmp = (d_callHistory[i]).second;
- return tmp;
- }
-
- OutputChannelCallType getIthCallType(int i) {
- return (d_callHistory[i]).first;
- }
-
- unsigned getNumCalls() {
- return d_callHistory.size();
- }
-};
-
-class DummyTheory : public Theory {
-public:
- set<Node> d_registered;
- vector<Node> d_getSequence;
-
- DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
- Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, qe) {
- }
-
- void registerTerm(TNode n) {
- // check that we registerTerm() a term only once
- TS_ASSERT(d_registered.find(n) == d_registered.end());
-
- for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
- // check that registerTerm() is called in reverse topological order
- TS_ASSERT(d_registered.find(*i) != d_registered.end());
- }
-
- d_registered.insert(n);
- }
-
- Node getWrapper() {
- Node n = get();
- d_getSequence.push_back(n);
- return n;
- }
-
- bool doneWrapper() {
- return done();
- }
-
- void check(Effort e) {
- while(!done()) {
- getWrapper();
- }
- }
-
- void presolve() {
- Unimplemented();
- }
- void preRegisterTerm(TNode n) {}
- void propagate(Effort level) {}
- 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;
- LogicInfo* d_logicInfo;
-
- TestOutputChannel d_outputChannel;
-
- DummyTheory* d_dummy;
-
- Node atom0;
- Node atom1;
-
-public:
-
- void setUp() {
- d_ctxt = new Context();
- d_uctxt = new UserContext();
- d_nm = new NodeManager(d_ctxt, NULL);
- d_scope = new NodeManagerScope(d_nm);
- d_logicInfo = new LogicInfo();
- d_logicInfo->lock();
- d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo, NULL);
- d_outputChannel.clear();
- atom0 = d_nm->mkConst(true);
- atom1 = d_nm->mkConst(false);
- }
-
- void tearDown() {
- atom1 = Node::null();
- atom0 = Node::null();
- delete d_dummy;
- delete d_logicInfo;
- delete d_scope;
- delete d_nm;
- delete d_uctxt;
- delete d_ctxt;
- }
-
- void testEffort(){
- Theory::Effort s = Theory::EFFORT_STANDARD;
- Theory::Effort f = Theory::EFFORT_FULL;
-
- TS_ASSERT( Theory::standardEffortOnly(s));
- TS_ASSERT(!Theory::standardEffortOnly(f));
-
- TS_ASSERT(!Theory::fullEffort(s));
- TS_ASSERT( Theory::fullEffort(f));
-
- TS_ASSERT( Theory::standardEffortOrMore(s));
- TS_ASSERT( Theory::standardEffortOrMore(f));
- }
-
- void testDone() {
- TS_ASSERT(d_dummy->doneWrapper());
-
- d_dummy->assertFact(atom0, true);
- d_dummy->assertFact(atom1, true);
-
- TS_ASSERT(!d_dummy->doneWrapper());
-
- d_dummy->check(Theory::EFFORT_FULL);
-
- TS_ASSERT(d_dummy->doneWrapper());
- }
-
- // FIXME: move this to theory_engine test?
-// void testRegisterTerm() {
-// TS_ASSERT(d_dummy->doneWrapper());
-
-// TypeNode typeX = d_nm->booleanType();
-// TypeNode typeF = d_nm->mkFunctionType(typeX, typeX);
-
-// Node x = d_nm->mkVar("x",typeX);
-// Node f = d_nm->mkVar("f",typeF);
-// Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
-// Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
-// Node f_x_eq_x = f_x.eqNode(x);
-// Node x_eq_f_f_x = x.eqNode(f_f_x);
-
-// d_dummy->assertFact(f_x_eq_x);
-// d_dummy->assertFact(x_eq_f_f_x);
-
-// Node got = d_dummy->getWrapper();
-
-// TS_ASSERT_EQUALS(got, f_x_eq_x);
-
-// TS_ASSERT_EQUALS(5u, d_dummy->d_registered.size());
-// TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end());
-// TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end());
-// TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end());
-// TS_ASSERT(d_dummy->d_registered.find(f_x_eq_x) != d_dummy->d_registered.end());
-// TS_ASSERT(d_dummy->d_registered.find(d_nm->operatorOf(kind::EQUAL)) != d_dummy->d_registered.end());
-// TS_ASSERT(d_dummy->d_registered.find(f_f_x) == d_dummy->d_registered.end());
-// TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) == d_dummy->d_registered.end());
-
-// TS_ASSERT(!d_dummy->doneWrapper());
-
-// got = d_dummy->getWrapper();
-
-// TS_ASSERT_EQUALS(got, x_eq_f_f_x);
-
-// TS_ASSERT_EQUALS(7u, d_dummy->d_registered.size());
-// TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end());
-// TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end());
-
-// TS_ASSERT(d_dummy->doneWrapper());
-// }
-
- void testOutputChannelAccessors() {
- /* void setOutputChannel(OutputChannel& out) */
- /* OutputChannel& getOutputChannel() */
-
- TestOutputChannel theOtherChannel;
-
- TS_ASSERT_EQUALS(&(d_dummy->getOutputChannel()), &d_outputChannel);
-
- d_dummy->setOutputChannel(theOtherChannel);
-
- TS_ASSERT_EQUALS(&(d_dummy->getOutputChannel()), &theOtherChannel);
-
- const OutputChannel& oc = d_dummy->getOutputChannel();
-
- TS_ASSERT_EQUALS(&oc, &theOtherChannel);
- }
-
- void testOutputChannel() {
- Node n = atom0.orNode(atom1);
- d_outputChannel.lemma(n, false);
- d_outputChannel.split(atom0);
- Node s = atom0.orNode(atom0.notNode());
- TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u);
- TS_ASSERT_EQUALS(d_outputChannel.d_callHistory[0], make_pair(LEMMA, n));
- TS_ASSERT_EQUALS(d_outputChannel.d_callHistory[1], make_pair(LEMMA, s));
- d_outputChannel.d_callHistory.clear();
- }
-};
#include "expr/node_manager.h"
#include "expr/kind.h"
#include "context/context.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "util/rational.h"
#include "util/integer.h"
#include "util/options.h"
using namespace CVC4::expr;
using namespace CVC4::context;
using namespace CVC4::kind;
+using namespace CVC4::smt;
using namespace std;
Context* d_ctxt;
UserContext* d_uctxt;
+ ExprManager* d_em;
NodeManager* d_nm;
- NodeManagerScope* d_scope;
+ SmtEngine* d_smt;
+ SmtScope* d_scope;
FakeOutputChannel *d_nullChannel;
TheoryEngine* d_theoryEngine;
- LogicInfo* d_logicInfo;
public:
void setUp() {
- d_ctxt = new Context();
- d_uctxt = new UserContext();
+ d_em = new ExprManager();
+ d_smt = new SmtEngine(d_em);
+ d_nm = NodeManager::fromExprManager(d_em);
+ d_scope = new SmtScope(d_smt);
- d_nm = new NodeManager(d_ctxt, NULL);
- d_scope = new NodeManagerScope(d_nm);
+ d_ctxt = d_smt->d_context;
+ d_uctxt = d_smt->d_userContext;
d_nullChannel = new FakeOutputChannel();
- // create the TheoryEngine
- d_logicInfo = new LogicInfo();
- d_theoryEngine = new TheoryEngine(d_ctxt, d_uctxt, *d_logicInfo);
-
+ d_theoryEngine = d_smt->d_theoryEngine;
+ for(TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) {
+ delete d_theoryEngine->d_theoryOut[id];
+ delete d_theoryEngine->d_theoryTable[id];
+ d_theoryEngine->d_theoryOut[id] = NULL;
+ d_theoryEngine->d_theoryTable[id] = NULL;
+ }
d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN);
d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL);
d_theoryEngine->addTheory< FakeTheory<THEORY_UF> >(THEORY_UF);
d_theoryEngine->addTheory< FakeTheory<THEORY_ARITH> >(THEORY_ARITH);
d_theoryEngine->addTheory< FakeTheory<THEORY_ARRAY> >(THEORY_ARRAY);
d_theoryEngine->addTheory< FakeTheory<THEORY_BV> >(THEORY_BV);
-
- //Debug.on("theory-rewrite");
}
void tearDown() {
- d_theoryEngine->shutdown();
- delete d_theoryEngine;
- delete d_logicInfo;
-
delete d_nullChannel;
delete d_scope;
- delete d_nm;
-
- delete d_uctxt;
- delete d_ctxt;
+ delete d_smt;
+ delete d_em;
}
void testRewriterSimple() {
--- /dev/null
+/********************* */
+/*! \file theory_black.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: barrett, mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::theory::Theory.
+ **
+ ** Black box testing of CVC4::theory::Theory.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "context/context.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+
+#include <vector>
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::expr;
+using namespace CVC4::context;
+using namespace CVC4::smt;
+
+using namespace std;
+
+/**
+ * Very basic OutputChannel for testing simple Theory Behaviour.
+ * Stores a call sequence for the output channel
+ */
+enum OutputChannelCallType{CONFLICT, PROPAGATE, LEMMA, EXPLANATION};
+class TestOutputChannel : public OutputChannel {
+private:
+ void push(OutputChannelCallType call, TNode n) {
+ d_callHistory.push_back(make_pair(call, n));
+ }
+
+public:
+ vector< pair<OutputChannelCallType, Node> > d_callHistory;
+
+ TestOutputChannel() {}
+
+ ~TestOutputChannel() {}
+
+ void safePoint() throw(Interrupted, AssertionException) {}
+
+ void conflict(TNode n)
+ throw(AssertionException) {
+ push(CONFLICT, n);
+ }
+
+ bool propagate(TNode n)
+ throw(AssertionException) {
+ push(PROPAGATE, n);
+ return true;
+ }
+
+ void propagateAsDecision(TNode n)
+ throw(AssertionException) {
+ // ignore
+ }
+
+ LemmaStatus lemma(TNode n, bool removable)
+ throw(AssertionException) {
+ push(LEMMA, n);
+ return LemmaStatus(Node::null(), 0);
+ }
+
+ void requirePhase(TNode, bool)
+ throw(Interrupted, AssertionException) {
+ Unreachable();
+ }
+
+ bool flipDecision()
+ throw(Interrupted, AssertionException) {
+ Unreachable();
+ }
+
+ void setIncomplete()
+ throw(AssertionException) {
+ Unreachable();
+ }
+
+ void clear() {
+ d_callHistory.clear();
+ }
+
+ Node getIthNode(int i) {
+ Node tmp = (d_callHistory[i]).second;
+ return tmp;
+ }
+
+ OutputChannelCallType getIthCallType(int i) {
+ return (d_callHistory[i]).first;
+ }
+
+ unsigned getNumCalls() {
+ return d_callHistory.size();
+ }
+};
+
+class DummyTheory : public Theory {
+public:
+ set<Node> d_registered;
+ vector<Node> d_getSequence;
+
+ DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
+ Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, qe) {
+ }
+
+ void registerTerm(TNode n) {
+ // check that we registerTerm() a term only once
+ TS_ASSERT(d_registered.find(n) == d_registered.end());
+
+ for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+ // check that registerTerm() is called in reverse topological order
+ TS_ASSERT(d_registered.find(*i) != d_registered.end());
+ }
+
+ d_registered.insert(n);
+ }
+
+ Node getWrapper() {
+ Node n = get();
+ d_getSequence.push_back(n);
+ return n;
+ }
+
+ bool doneWrapper() {
+ return done();
+ }
+
+ void check(Effort e) {
+ while(!done()) {
+ getWrapper();
+ }
+ }
+
+ void presolve() {
+ Unimplemented();
+ }
+ void preRegisterTerm(TNode n) {}
+ void propagate(Effort level) {}
+ 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;
+ ExprManager* d_em;
+ SmtScope* d_scope;
+ SmtEngine* d_smt;
+ LogicInfo* d_logicInfo;
+
+ TestOutputChannel d_outputChannel;
+
+ DummyTheory* d_dummy;
+
+ Node atom0;
+ Node atom1;
+
+public:
+
+ void setUp() {
+ d_em = new ExprManager();
+ d_nm = NodeManager::fromExprManager(d_em);
+ d_smt = new SmtEngine(d_em);
+ d_ctxt = d_smt->d_context;
+ d_uctxt = d_smt->d_userContext;
+ d_scope = new SmtScope(d_smt);
+ d_logicInfo = new LogicInfo();
+ d_logicInfo->lock();
+
+ // guard against duplicate statistics assertion errors
+ delete d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN];
+ delete d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN];
+ d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL;
+ d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL;
+
+ d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo, NULL);
+ d_outputChannel.clear();
+ atom0 = d_nm->mkConst(true);
+ atom1 = d_nm->mkConst(false);
+ }
+
+ void tearDown() {
+ atom1 = Node::null();
+ atom0 = Node::null();
+ delete d_dummy;
+ delete d_logicInfo;
+ delete d_scope;
+ delete d_smt;
+ delete d_em;
+ }
+
+ void testEffort(){
+ Theory::Effort s = Theory::EFFORT_STANDARD;
+ Theory::Effort f = Theory::EFFORT_FULL;
+
+ TS_ASSERT( Theory::standardEffortOnly(s));
+ TS_ASSERT(!Theory::standardEffortOnly(f));
+
+ TS_ASSERT(!Theory::fullEffort(s));
+ TS_ASSERT( Theory::fullEffort(f));
+
+ TS_ASSERT( Theory::standardEffortOrMore(s));
+ TS_ASSERT( Theory::standardEffortOrMore(f));
+ }
+
+ void testDone() {
+ TS_ASSERT(d_dummy->doneWrapper());
+
+ d_dummy->assertFact(atom0, true);
+ d_dummy->assertFact(atom1, true);
+
+ TS_ASSERT(!d_dummy->doneWrapper());
+
+ d_dummy->check(Theory::EFFORT_FULL);
+
+ TS_ASSERT(d_dummy->doneWrapper());
+ }
+
+ // FIXME: move this to theory_engine test?
+// void testRegisterTerm() {
+// TS_ASSERT(d_dummy->doneWrapper());
+
+// TypeNode typeX = d_nm->booleanType();
+// TypeNode typeF = d_nm->mkFunctionType(typeX, typeX);
+
+// Node x = d_nm->mkVar("x",typeX);
+// Node f = d_nm->mkVar("f",typeF);
+// Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
+// Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
+// Node f_x_eq_x = f_x.eqNode(x);
+// Node x_eq_f_f_x = x.eqNode(f_f_x);
+
+// d_dummy->assertFact(f_x_eq_x);
+// d_dummy->assertFact(x_eq_f_f_x);
+
+// Node got = d_dummy->getWrapper();
+
+// TS_ASSERT_EQUALS(got, f_x_eq_x);
+
+// TS_ASSERT_EQUALS(5u, d_dummy->d_registered.size());
+// TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end());
+// TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end());
+// TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end());
+// TS_ASSERT(d_dummy->d_registered.find(f_x_eq_x) != d_dummy->d_registered.end());
+// TS_ASSERT(d_dummy->d_registered.find(d_nm->operatorOf(kind::EQUAL)) != d_dummy->d_registered.end());
+// TS_ASSERT(d_dummy->d_registered.find(f_f_x) == d_dummy->d_registered.end());
+// TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) == d_dummy->d_registered.end());
+
+// TS_ASSERT(!d_dummy->doneWrapper());
+
+// got = d_dummy->getWrapper();
+
+// TS_ASSERT_EQUALS(got, x_eq_f_f_x);
+
+// TS_ASSERT_EQUALS(7u, d_dummy->d_registered.size());
+// TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end());
+// TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end());
+
+// TS_ASSERT(d_dummy->doneWrapper());
+// }
+
+ void testOutputChannelAccessors() {
+ /* void setOutputChannel(OutputChannel& out) */
+ /* OutputChannel& getOutputChannel() */
+
+ TestOutputChannel theOtherChannel;
+
+ TS_ASSERT_EQUALS(&(d_dummy->getOutputChannel()), &d_outputChannel);
+
+ d_dummy->setOutputChannel(theOtherChannel);
+
+ TS_ASSERT_EQUALS(&(d_dummy->getOutputChannel()), &theOtherChannel);
+
+ const OutputChannel& oc = d_dummy->getOutputChannel();
+
+ TS_ASSERT_EQUALS(&oc, &theOtherChannel);
+ }
+
+ void testOutputChannel() {
+ Node n = atom0.orNode(atom1);
+ d_outputChannel.lemma(n, false);
+ d_outputChannel.split(atom0);
+ Node s = atom0.orNode(atom0.notNode());
+ TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u);
+ TS_ASSERT_EQUALS(d_outputChannel.d_callHistory[0], make_pair(LEMMA, n));
+ TS_ASSERT_EQUALS(d_outputChannel.d_callHistory[1], make_pair(LEMMA, s));
+ d_outputChannel.d_callHistory.clear();
+ }
+};
projects / cvc5.git / commitdiff