diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/bitblaster.cpp | 2 | ||||
-rw-r--r-- | src/theory/logic_info.cpp | 7 | ||||
-rw-r--r-- | src/theory/logic_info.h | 3 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 4 |
4 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index aca81e176..91482526a 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -100,7 +100,7 @@ void Bitblaster::bbAtom(TNode node) { Node atom_definition = mkNode(kind::IFF, node, atom_bb); if (!options::bitvectorEagerBitblast()) { - d_cnfStream->convertAndAssert(atom_definition, true, false); + d_cnfStream->convertAndAssert(atom_definition, false, false); d_bitblastedAtoms.insert(node); } else { d_bvOutput->lemma(atom_definition, false); diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index e76e2ace9..f90bee19d 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -31,7 +31,7 @@ namespace CVC4 { LogicInfo::LogicInfo() : d_logicString(""), - d_theories(), + d_theories(THEORY_LAST, false), d_sharingTheories(0), d_integers(true), d_reals(true), @@ -40,14 +40,13 @@ LogicInfo::LogicInfo() : d_locked(false) { for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { - d_theories[id] = false;// ensure it's cleared enableTheory(id); } } LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) : d_logicString(""), - d_theories(), + d_theories(THEORY_LAST, false), d_sharingTheories(0), d_integers(false), d_reals(false), @@ -61,7 +60,7 @@ LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) : LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : d_logicString(""), - d_theories(), + d_theories(THEORY_LAST, false), d_sharingTheories(0), d_integers(false), d_reals(false), diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index e2d8f3da6..fd81ea629 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -22,6 +22,7 @@ #define __CVC4__LOGIC_INFO_H #include <string> +#include <vector> #include "expr/kind.h" namespace CVC4 { @@ -43,7 +44,7 @@ namespace CVC4 { */ class CVC4_PUBLIC LogicInfo { mutable std::string d_logicString; /**< an SMT-LIB-like logic string */ - bool d_theories[theory::THEORY_LAST]; /**< set of active theories */ + std::vector<bool> d_theories; /**< set of active theories */ size_t d_sharingTheories; /**< count of theories that need sharing */ // for arithmetic diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index cd3b34879..60d79e90e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -341,7 +341,7 @@ void TheoryEngine::check(Theory::Effort effort) { Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas") << std::endl; } catch(const theory::Interrupted&) { - Trace("theory") << "TheoryEngine::check() => conflict" << endl; + Trace("theory") << "TheoryEngine::check() => interrupted" << endl; } // If fulleffort, check all theories @@ -519,7 +519,7 @@ bool TheoryEngine::properConflict(TNode conflict) const { } bool TheoryEngine::properPropagation(TNode lit) const { - if(!getPropEngine()->isTranslatedSatLiteral(lit)) { + if(!getPropEngine()->isSatLiteral(lit)) { return false; } bool b; |