** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
- **
+ **
**/
#include "bitblaster.h"
using namespace std;
using namespace CVC4::theory::bv::utils;
-using namespace CVC4::context;
+using namespace CVC4::context;
using namespace CVC4::prop;
namespace CVC4 {
namespace bv{
std::string toString(Bits& bits) {
- ostringstream os;
+ ostringstream os;
for (int i = bits.size() - 1; i >= 0; --i) {
TNode bit = bits[i];
if (bit.getKind() == kind::CONST_BOOLEAN) {
os << (bit.getConst<bool>() ? "1" : "0");
} else {
- os << bit<< " ";
+ os << bit<< " ";
}
}
os <<"\n";
-
- return os.str();
+
+ return os.str();
}
-/////// Bitblaster
+/////// Bitblaster
Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) :
d_bv(bv),
d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar(), new Context());
MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv);
- d_satSolver->setNotify(notify);
+ d_satSolver->setNotify(notify);
// initializing the bit-blasting strategies
- initAtomBBStrategies();
- initTermBBStrategies();
+ initAtomBBStrategies();
+ initTermBBStrategies();
}
Bitblaster::~Bitblaster() {
delete d_cnfStream;
- delete d_satSolver;
+ delete d_satSolver;
}
-/**
+/**
* Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
* NOTE: duplicate clauses are not detected because of marker literal
* @param node the atom to be bitblasted
- *
+ *
*/
void Bitblaster::bbAtom(TNode node) {
node = node.getKind() == kind::NOT? node[0] : node;
-
+
if (hasBBAtom(node)) {
- return;
+ return;
}
// make sure it is marked as an atom
- addAtom(node);
+ addAtom(node);
- Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
+ Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
++d_statistics.d_numAtoms;
// the bitblasted definition of the atom
Node normalized = Rewriter::rewrite(node);
return;
}
- Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
+ Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
++d_statistics.d_numTerms;
d_termBBStrategies[node.getKind()] (node, bits,this);
-
+
Assert (bits.size() == utils::getSize(node));
- cacheTermDef(node, bits);
+ cacheTermDef(node, bits);
}
Node Bitblaster::bbOptimize(TNode node) {
if (node.getKind() == kind::BITVECTOR_PLUS) {
if (RewriteRule<BBPlusNeg>::applies(node)) {
Node res = RewriteRule<BBPlusNeg>::run<false>(node);
- return res;
+ return res;
}
// if (RewriteRule<BBFactorOut>::applies(node)) {
// Node res = RewriteRule<BBFactorOut>::run<false>(node);
- // return res;
- // }
+ // return res;
+ // }
} else if (node.getKind() == kind::BITVECTOR_MULT) {
if (RewriteRule<MultPow2>::applies(node)) {
Node res = RewriteRule<MultPow2>::run<false>(node);
- return res;
+ return res;
}
}
-
- return node;
+
+ return node;
}
/// Public methods
std::vector<SatLiteral> literal_explanation;
d_satSolver->explain(d_cnfStream->getLiteral(atom), literal_explanation);
for (unsigned i = 0; i < literal_explanation.size(); ++i) {
- explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
+ explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
}
}
-/**
+/**
* Asserts the clauses corresponding to the atom to the Sat Solver
* by turning on the marker literal (i.e. setting it to false)
* @param node the atom to be asserted
- *
+ *
*/
-
+
bool Bitblaster::propagate() {
return d_satSolver->propagate() == prop::SAT_VALUE_TRUE;
}
bool Bitblaster::assertToSat(TNode lit, bool propagate) {
// strip the not
- TNode atom;
+ TNode atom;
if (lit.getKind() == kind::NOT) {
- atom = lit[0];
+ atom = lit[0];
} else {
- atom = lit;
+ atom = lit;
}
-
+
Assert (hasBBAtom(atom));
SatLiteral markerLit = d_cnfStream->getLiteral(atom);
if(lit.getKind() == kind::NOT) {
markerLit = ~markerLit;
}
-
+
Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n";
- Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal: " << markerLit << "\n";
+ Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal: " << markerLit << "\n";
SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
return ret == prop::SAT_VALUE_TRUE;
}
-/**
- * Calls the solve method for the Sat Solver.
+/**
+ * Calls the solve method for the Sat Solver.
* passing it the marker literals to be asserted
- *
+ *
* @return true for sat, and false for unsat
*/
-
+
bool Bitblaster::solve(bool quick_solve) {
if (Trace.isOn("bitvector")) {
Trace("bitvector") << "Bitblaster::solve() asserted atoms ";
Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n";
}
}
- Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n";
- return SAT_VALUE_TRUE == d_satSolver->solve();
+ Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n";
+ return SAT_VALUE_TRUE == d_satSolver->solve();
}
void Bitblaster::getConflict(std::vector<TNode>& conflict) {
SatClause conflictClause;
d_satSolver->getUnsatCore(conflictClause);
-
+
for (unsigned i = 0; i < conflictClause.size(); i++) {
- SatLiteral lit = conflictClause[i];
+ SatLiteral lit = conflictClause[i];
TNode atom = d_cnfStream->getNode(lit);
- Node not_atom;
+ Node not_atom;
if (atom.getKind() == kind::NOT) {
not_atom = atom[0];
} else {
- not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom);
+ not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom);
}
- conflict.push_back(not_atom);
+ conflict.push_back(not_atom);
}
}
void Bitblaster::initAtomBBStrategies() {
for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
- d_atomBBStrategies[i] = UndefinedAtomBBStrategy;
+ d_atomBBStrategies[i] = UndefinedAtomBBStrategy;
}
-
+
/// setting default bb strategies for atoms
d_atomBBStrategies [ kind::EQUAL ] = DefaultEqBB;
d_atomBBStrategies [ kind::BITVECTOR_ULT ] = DefaultUltBB;
d_atomBBStrategies [ kind::BITVECTOR_SLE ] = DefaultSleBB;
d_atomBBStrategies [ kind::BITVECTOR_SGT ] = DefaultSgtBB;
d_atomBBStrategies [ kind::BITVECTOR_SGE ] = DefaultSgeBB;
-
+
}
void Bitblaster::initTermBBStrategies() {
for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
d_termBBStrategies[i] = DefaultVarBB;
}
-
+
/// setting default bb strategies for terms:
// d_termBBStrategies [ kind::VARIABLE ] = DefaultVarBB;
d_termBBStrategies [ kind::CONST_BITVECTOR ] = DefaultConstBB;
d_termBBStrategies [ kind::BITVECTOR_PLUS ] = DefaultPlusBB;
d_termBBStrategies [ kind::BITVECTOR_SUB ] = DefaultSubBB;
d_termBBStrategies [ kind::BITVECTOR_NEG ] = DefaultNegBB;
- d_termBBStrategies [ kind::BITVECTOR_UDIV ] = UndefinedTermBBStrategy;
- d_termBBStrategies [ kind::BITVECTOR_UREM ] = UndefinedTermBBStrategy;
+ d_termBBStrategies [ kind::BITVECTOR_UDIV ] = UndefinedTermBBStrategy;
+ d_termBBStrategies [ kind::BITVECTOR_UREM ] = UndefinedTermBBStrategy;
d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ] = DefaultUdivBB;
d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ] = DefaultUremBB;
- d_termBBStrategies [ kind::BITVECTOR_SDIV ] = UndefinedTermBBStrategy;
- d_termBBStrategies [ kind::BITVECTOR_SREM ] = UndefinedTermBBStrategy;
- d_termBBStrategies [ kind::BITVECTOR_SMOD ] = UndefinedTermBBStrategy;
+ d_termBBStrategies [ kind::BITVECTOR_SDIV ] = UndefinedTermBBStrategy;
+ d_termBBStrategies [ kind::BITVECTOR_SREM ] = UndefinedTermBBStrategy;
+ d_termBBStrategies [ kind::BITVECTOR_SMOD ] = UndefinedTermBBStrategy;
d_termBBStrategies [ kind::BITVECTOR_SHL ] = DefaultShlBB;
d_termBBStrategies [ kind::BITVECTOR_LSHR ] = DefaultLshrBB;
d_termBBStrategies [ kind::BITVECTOR_ASHR ] = DefaultAshrBB;
d_termBBStrategies [ kind::BITVECTOR_ROTATE_LEFT ] = DefaultRotateLeftBB;
}
-
+
bool Bitblaster::hasBBAtom(TNode atom) const {
return d_bitblastedAtoms.find(atom) != d_bitblastedAtoms.end();
}
void Bitblaster::cacheTermDef(TNode term, Bits def) {
Assert (d_termCache.find(term) == d_termCache.end());
- d_termCache[term] = def;
+ d_termCache[term] = def;
}
bool Bitblaster::hasBBTerm(TNode node) const {
- return d_termCache.find(node) != d_termCache.end();
+ return d_termCache.find(node) != d_termCache.end();
}
void Bitblaster::getBBTerm(TNode node, Bits& bits) const {
- Assert (hasBBTerm(node));
+ Assert (hasBBTerm(node));
// copy?
bits = d_termCache.find(node)->second;
}
d_numTermClauses("theory::bv::NumberOfTermSatClauses", 0),
d_numAtomClauses("theory::bv::NumberOfAtomSatClauses", 0),
d_numTerms("theory::bv::NumberOfBitblastedTerms", 0),
- d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0),
+ d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0),
d_bitblastTimer("theory::bv::BitblastTimer")
{
StatisticsRegistry::registerStat(&d_numTermClauses);
};
void Bitblaster::MinisatNotify::safePoint() {
- d_bv->d_out->safePoint();
+ d_bv->d_out->safePoint();
}
EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) {
bool Bitblaster::isSharedTerm(TNode node) {
- return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
+ return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
}
bool Bitblaster::hasValue(TNode a) {
- Assert (d_termCache.find(a) != d_termCache.end());
+ Assert (d_termCache.find(a) != d_termCache.end());
Bits bits = d_termCache[a];
for (int i = bits.size() -1; i >= 0; --i) {
- SatValue bit_value;
- if (d_cnfStream->hasLiteral(bits[i])) {
+ SatValue bit_value;
+ if (d_cnfStream->hasLiteral(bits[i])) {
SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
bit_value = d_satSolver->value(bit);
if (bit_value == SAT_VALUE_UNKNOWN)
- return false;
+ return false;
} else {
- return false;
+ return false;
}
}
- return true;
+ return true;
}
-/**
+/**
* Returns the value a is currently assigned to in the SAT solver
- * or null if the value is completely unassigned.
- *
- * @param a
- *
- * @return
+ * or null if the value is completely unassigned.
+ *
+ * @param a
+ *
+ * @return
*/
-Node Bitblaster::getVarValue(TNode a) {
+Node Bitblaster::getVarValue(TNode a, bool fullModel) {
if (d_termCache.find(a) == d_termCache.end()) {
Assert(isSharedTerm(a));
- return Node();
+ return Node();
}
Bits bits = d_termCache[a];
- Integer value(0);
+ Integer value(0);
for (int i = bits.size() -1; i >= 0; --i) {
SatValue bit_value;
- if (d_cnfStream->hasLiteral(bits[i])) {
+ if (d_cnfStream->hasLiteral(bits[i])) {
SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
bit_value = d_satSolver->value(bit);
- Assert (bit_value != SAT_VALUE_UNKNOWN);
+ Assert (bit_value != SAT_VALUE_UNKNOWN);
} else {
- // the bit is unconstrainted so we can give it an arbitrary value
+ //TODO: return Node() if fullModel=false?
+ // the bit is unconstrainted so we can give it an arbitrary value
bit_value = SAT_VALUE_FALSE;
}
- Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0);
- value = value * 2 + bit_int;
+ Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0);
+ value = value * 2 + bit_int;
}
- return utils::mkConst(BitVector(bits.size(), value));
+ return utils::mkConst(BitVector(bits.size(), value));
}
-void Bitblaster::collectModelInfo(TheoryModel* m) {
+void Bitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
__gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin();
for (; it!= d_variables.end(); ++it) {
TNode var = *it;
if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) {
- Node const_value = getVarValue(var);
+ Node const_value = getVarValue(var, fullModel);
if(const_value == Node()) {
- // if the value is unassigned just set it to zero
- const_value = utils::mkConst(BitVector(utils::getSize(var), 0u));
+ if( fullModel ){
+ // if the value is unassigned just set it to zero
+ const_value = utils::mkConst(BitVector(utils::getSize(var), 0u));
+ }
+ }
+ if(const_value != Node()) {
+ Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
+ << var << " "
+ << const_value << "))\n";
+ m->assertEquality(var, const_value, true);
}
- Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
- << var << " "
- << const_value << "))\n";
- m->assertEquality(var, const_value, true);
}
}
}
typedef std::vector<Node> Bits;
-std::string toString (Bits& bits);
+std::string toString (Bits& bits);
class TheoryBV;
-/**
- * The Bitblaster that manages the mapping between Nodes
- * and their bitwise definition
- *
+/**
+ * The Bitblaster that manages the mapping between Nodes
+ * and their bitwise definition
+ *
*/
class Bitblaster {
void notify(prop::SatClause& clause);
void safePoint();
};
-
-
+
+
typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction > TermDefMap;
typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet;
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> VarSet;
-
- typedef void (*TermBBStrategy) (TNode, Bits&, Bitblaster*);
- typedef Node (*AtomBBStrategy) (TNode, Bitblaster*);
+ typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> VarSet;
+
+ typedef void (*TermBBStrategy) (TNode, Bits&, Bitblaster*);
+ typedef Node (*AtomBBStrategy) (TNode, Bitblaster*);
TheoryBV *d_bv;
-
+
// sat solver used for bitblasting and associated CnfStream
theory::OutputChannel* d_bvOutput;
- prop::BVSatSolverInterface* d_satSolver;
+ prop::BVSatSolverInterface* d_satSolver;
prop::CnfStream* d_cnfStream;
// caches and mappings
TermDefMap d_termCache;
AtomSet d_bitblastedAtoms;
- VarSet d_variables;
+ VarSet d_variables;
context::CDList<prop::SatLiteral> d_assertedAtoms; /**< context dependent list storing the atoms
currently asserted by the DPLL SAT solver. */
/// function tables for the various bitblasting strategies indexed by node kind
TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
- AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
+ AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
// helper methods to initialize function tables
void initAtomBBStrategies();
- void initTermBBStrategies();
+ void initTermBBStrategies();
// returns a node that might be easier to bitblast
- Node bbOptimize(TNode node);
-
- void addAtom(TNode atom);
+ Node bbOptimize(TNode node);
+
+ void addAtom(TNode atom);
// division is bitblasted in terms of constraints
// so it needs to use private bitblaster interface
void bbUdiv(TNode node, Bits& bits);
void bbUrem(TNode node, Bits& bits);
- bool hasValue(TNode a);
+ bool hasValue(TNode a);
public:
void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division
void bbTerm(TNode node, Bits& bits);
void bbAtom(TNode node);
-
- Bitblaster(context::Context* c, bv::TheoryBV* bv);
+
+ Bitblaster(context::Context* c, bv::TheoryBV* bv);
~Bitblaster();
bool assertToSat(TNode node, bool propagate = true);
bool propagate();
bool solve(bool quick_solve = false);
- void getConflict(std::vector<TNode>& conflict);
+ void getConflict(std::vector<TNode>& conflict);
void explain(TNode atom, std::vector<TNode>& explanation);
EqualityStatus getEqualityStatus(TNode a, TNode b);
- /**
+ /**
* Return a constant Node representing the value of a variable
- * in the current model.
- * @param a
- *
- * @return
+ * in the current model.
+ * @param a
+ *
+ * @return
*/
- Node getVarValue(TNode a);
- /**
- * Adds a constant value for each bit-blasted variable in the model.
- *
- * @param m the model
+ Node getVarValue(TNode a, bool fullModel=true);
+ /**
+ * Adds a constant value for each bit-blasted variable in the model.
+ *
+ * @param m the model
*/
- void collectModelInfo(TheoryModel* m);
- /**
- * Stores the variable (or non-bv term) and its corresponding bits.
- *
- * @param var
- * @param bits
+ void collectModelInfo(TheoryModel* m, bool fullModel);
+ /**
+ * Stores the variable (or non-bv term) and its corresponding bits.
+ *
+ * @param var
+ * @param bits
*/
void storeVariable(TNode var) {
- d_variables.insert(var);
+ d_variables.insert(var);
}
bool isSharedTerm(TNode node);
uint64_t computeAtomWeight(TNode node);
private:
-
+
class Statistics {
public:
IntStat d_numTermClauses, d_numAtomClauses;
- IntStat d_numTerms, d_numAtoms;
+ IntStat d_numTerms, d_numAtoms;
TimerStat d_bitblastTimer;
Statistics();
- ~Statistics();
- };
-
+ ~Statistics();
+ };
+
Statistics d_statistics;
};
-} /* bv namespace */
+} /* bv namespace */
} /* theory namespace */
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Algebraic solver.
+ ** \brief Algebraic solver.
**
** Algebraic solver.
**/
out << "BV_CORE_SUBTHEORY";
break;
case SUB_INEQUALITY:
- out << "BV_INEQUALITY_SUBTHEORY";
+ out << "BV_INEQUALITY_SUBTHEORY";
default:
Unreachable();
break;
}
-// forward declaration
-class TheoryBV;
+// forward declaration
+class TheoryBV;
-typedef context::CDQueue<Node> AssertionQueue;
+typedef context::CDQueue<Node> AssertionQueue;
/**
* Abstract base class for bit-vector subtheory solvers
*
AssertionQueue d_assertionQueue;
context::CDO<uint32_t> d_assertionIndex;
public:
-
+
SubtheorySolver(context::Context* c, TheoryBV* bv) :
d_context(c),
d_bv(bv),
d_assertionIndex(c, 0)
{}
virtual ~SubtheorySolver() {}
- virtual bool check(Theory::Effort e) = 0;
+ virtual bool check(Theory::Effort e) = 0;
virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
virtual void preRegister(TNode node) {}
virtual void propagate(Theory::Effort e) {}
- virtual void collectModelInfo(TheoryModel* m) = 0;
- virtual Node getModelValue(TNode var) = 0;
+ virtual void collectModelInfo(TheoryModel* m, bool fullModel) = 0;
+ virtual Node getModelValue(TNode var) = 0;
virtual bool isComplete() = 0;
virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
- virtual void addSharedTerm(TNode node) {}
+ virtual void addSharedTerm(TNode node) {}
bool done() { return d_assertionQueue.size() == d_assertionIndex; }
TNode get() {
- Assert (!done());
+ Assert (!done());
TNode res = d_assertionQueue[d_assertionIndex];
d_assertionIndex = d_assertionIndex + 1;
- return res;
+ return res;
}
virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
-};
+};
}
}
}
bool BitblastSolver::check(Theory::Effort e) {
- Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
+ Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
Assert(!options::bitvectorEagerBitblast());
- ++(d_statistics.d_numCallstoCheck);
+ ++(d_statistics.d_numCallstoCheck);
//// Lazy bit-blasting
// bit-blast enqueued nodes
bitblastQueue();
- // Processing assertions
+ // Processing assertions
while (!done()) {
TNode fact = get();
d_validModelCache = false;
- Debug("bv-bitblast") << " fact " << fact << ")\n";
+ Debug("bv-bitblast") << " fact " << fact << ")\n";
if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
// Some atoms have not been bit-blasted yet
d_bitblaster->bbAtom(fact);
return d_bitblaster->getEqualityStatus(a, b);
}
-void BitblastSolver::collectModelInfo(TheoryModel* m) {
- return d_bitblaster->collectModelInfo(m);
+void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+ return d_bitblaster->collectModelInfo(m, fullModel);
}
Node BitblastSolver::getModelValue(TNode node)
Assert(val.isConst());
d_modelCache[node] = val;
Debug("bitvector-model") << node << " => " << val <<"\n";
- return val;
+ return val;
}
struct Statistics {
IntStat d_numCallstoCheck;
Statistics();
- ~Statistics();
- };
+ ~Statistics();
+ };
/** Bitblaster */
Bitblaster* d_bitblaster;
/** Nodes that still need to be bit-blasted */
context::CDQueue<TNode> d_bitblastQueue;
- Statistics d_statistics;
+ Statistics d_statistics;
typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
NodeMap d_modelCache;
context::CDO<bool> d_validModelCache;
Node getModelValueRec(TNode node);
- bool d_useSatPropagation;
+ bool d_useSatPropagation;
public:
BitblastSolver(context::Context* c, TheoryBV* bv);
~BitblastSolver();
bool check(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions);
EqualityStatus getEqualityStatus(TNode a, TNode b);
- void collectModelInfo(TheoryModel* m);
+ void collectModelInfo(TheoryModel* m, bool fullModel);
Node getModelValue(TNode node);
bool isComplete() { return true; }
void bitblastQueue();
}
CoreSolver::~CoreSolver() {
- delete d_slicer;
+ delete d_slicer;
}
void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
std::vector<Node> a_decomp;
d_slicer->getBaseDecomposition(a, a_decomp);
Node new_a = utils::mkConcat(a_decomp);
- Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n";
- return new_a;
+ Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n";
+ return new_a;
}
bool CoreSolver::decomposeFact(TNode fact) {
- Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
+ Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
// assert decompositions since the equality engine does not know the semantics of
// concat:
// a == a_1 concat ... concat a_k
// b == b_1 concat ... concat b_k
- Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
- // FIXME: are this the right things to assert?
+ Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
+ // FIXME: are this the right things to assert?
// assert decompositions since the equality engine does not know the semantics of
// concat:
// a == a_1 concat ... concat a_k
// b == b_1 concat ... concat b_k
- TNode eq = fact.getKind() == kind::NOT? fact[0] : fact;
+ TNode eq = fact.getKind() == kind::NOT? fact[0] : fact;
TNode a = eq[0];
TNode b = eq[1];
Node new_a = getBaseDecomposition(a);
- Node new_b = getBaseDecomposition(b);
-
+ Node new_b = getBaseDecomposition(b);
+
Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
- utils::getSize(new_a) == utils::getSize(a));
-
+ utils::getSize(new_a) == utils::getSize(a));
+
NodeManager* nm = NodeManager::currentNM();
Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b);
bool ok = true;
ok = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue());
- if (!ok) return false;
+ if (!ok) return false;
ok = assertFactToEqualityEngine(b_eq_new_b, utils::mkTrue());
- if (!ok) return false;
+ if (!ok) return false;
ok = assertFactToEqualityEngine(fact, fact);
if (!ok) return false;
-
+
if (fact.getKind() == kind::EQUAL) {
// assert the individual equalities as well
// a_i == b_i
if (new_a.getKind() == kind::BITVECTOR_CONCAT &&
new_b.getKind() == kind::BITVECTOR_CONCAT) {
-
- Assert (new_a.getNumChildren() == new_b.getNumChildren());
+
+ Assert (new_a.getNumChildren() == new_b.getNumChildren());
for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
ok = assertFactToEqualityEngine(eq_i, fact);
}
}
}
- return true;
+ return true;
}
bool CoreSolver::check(Theory::Effort e) {
Trace("bitvector::core") << "CoreSolver::check \n";
Assert (!d_bv->inConflict());
- ++(d_statistics.d_numCallstoCheck);
- bool ok = true;
+ ++(d_statistics.d_numCallstoCheck);
+ bool ok = true;
std::vector<Node> core_eqs;
while (! done()) {
- TNode fact = get();
-
+ TNode fact = get();
+
// update whether we are in the core fragment
if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) {
- d_isCoreTheory = false;
+ d_isCoreTheory = false;
}
-
+
// only reason about equalities
if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
if (options::bitvectorCoreSolver()) {
ok = assertFactToEqualityEngine(fact, fact);
}
} else {
- ok = assertFactToEqualityEngine(fact, fact);
+ ok = assertFactToEqualityEngine(fact, fact);
}
if (!ok)
- return false;
+ return false;
}
-
+
if (Theory::fullEffort(e) && isComplete()) {
buildModel();
}
-
+
return true;
}
void CoreSolver::buildModel() {
if (options::bitvectorCoreSolver()) {
// FIXME
- Unreachable();
- return;
+ Unreachable();
+ return;
}
- Debug("bv-core") << "CoreSolver::buildModel() \n";
- d_modelValues.clear();
+ Debug("bv-core") << "CoreSolver::buildModel() \n";
+ d_modelValues.clear();
TNodeSet constants;
- TNodeSet constants_in_eq_engine;
+ TNodeSet constants_in_eq_engine;
// collect constants in equality engine
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
while (!eqcs_i.isFinished()) {
TNode repr = *eqcs_i;
if (repr.getKind() == kind::CONST_BITVECTOR) {
eq::EqClassIterator it(repr, &d_equalityEngine);
if (!(++it).isFinished() || true) {
constants.insert(repr);
- constants_in_eq_engine.insert(repr);
+ constants_in_eq_engine.insert(repr);
}
}
- ++eqcs_i;
+ ++eqcs_i;
}
// build repr to value map
-
+
eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
while (!eqcs_i.isFinished()) {
TNode repr = *eqcs_i;
++eqcs_i;
-
+
if (repr.getKind() != kind::VARIABLE &&
repr.getKind() != kind::SKOLEM &&
repr.getKind() != kind::CONST_BITVECTOR &&
!d_bv->isSharedTerm(repr)) {
- continue;
+ continue;
}
-
- TypeNode type = repr.getType();
+
+ TypeNode type = repr.getType();
if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) {
- Debug("bv-core-model") << " processing " << repr <<"\n";
+ Debug("bv-core-model") << " processing " << repr <<"\n";
// we need to assign a value for it
TypeEnumerator te(type);
- Node val;
+ Node val;
do {
- val = *te;
+ val = *te;
++te;
// Debug("bv-core-model") << " trying value " << val << "\n";
// Debug("bv-core-model") << " is in set? " << constants.count(val) << "\n";
- // Debug("bv-core-model") << " enumerator done? " << te.isFinished() << "\n";
+ // Debug("bv-core-model") << " enumerator done? " << te.isFinished() << "\n";
} while (constants.count(val) != 0 && !(te.isFinished()));
-
+
if (te.isFinished() && constants.count(val) != 0) {
// if we cannot enumerate anymore values we just return the lemma stating that
// at least two of the representatives are equal.
for (TNodeSet::const_iterator it = constants_in_eq_engine.begin();
it != constants_in_eq_engine.end(); ++it) {
- TNode constant = *it;
+ TNode constant = *it;
if (utils::getSize(constant) == utils::getSize(repr)) {
- representatives.push_back(constant);
+ representatives.push_back(constant);
}
}
for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
representatives.push_back(it->first);
}
- std::vector<Node> equalities;
+ std::vector<Node> equalities;
for (unsigned i = 0; i < representatives.size(); ++i) {
for (unsigned j = i + 1; j < representatives.size(); ++j) {
TNode a = representatives[i];
}
Node lemma = utils::mkOr(equalities);
d_bv->lemma(lemma);
- Debug("bv-core") << " lemma: " << lemma << "\n";
- return;
+ Debug("bv-core") << " lemma: " << lemma << "\n";
+ return;
}
Debug("bv-core-model") << " " << repr << " => " << val <<"\n" ;
constants.insert(val);
- d_modelValues[repr] = val;
+ d_modelValues[repr] = val;
}
}
}
bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
- // Notify the equality engine
+ // Notify the equality engine
if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
// Debug("bv-slicer-eq") << " reason=" << reason << endl;
// checking for a conflict
if (d_bv->inConflict()) {
return false;
- }
- return true;
+ }
+ return true;
}
bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
d_bv->setConflict(conflict);
}
-void CoreSolver::collectModelInfo(TheoryModel* m) {
+void CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
if (options::bitvectorCoreSolver()) {
Unreachable();
- return;
+ return;
}
if (Debug.isOn("bitvector-model")) {
context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
d_bv->computeRelevantTerms(termSet);
m->assertEqualityEngine(&d_equalityEngine, &termSet);
if (isComplete()) {
- Debug("bitvector-model") << "CoreSolver::collectModelInfo complete.";
+ Debug("bitvector-model") << "CoreSolver::collectModelInfo complete.";
for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
Node a = it->first;
Node b = it->second;
- m->assertEquality(a, b, true);
+ m->assertEquality(a, b, true);
}
}
}
// we don't need to evaluate bv expressions and only look at variable values
// because this only gets called when the core theory is complete (i.e. no other bv
// function symbols are currently asserted)
- Assert (d_slicer->isCoreTerm(var));
-
- Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";
+ Assert (d_slicer->isCoreTerm(var));
+
+ Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";
Assert (isComplete());
TNode repr = d_equalityEngine.getRepresentative(var);
- Node result = Node();
+ Node result = Node();
if (repr.getKind() == kind::CONST_BITVECTOR) {
- result = repr;
+ result = repr;
} else if (d_modelValues.find(repr) == d_modelValues.end()) {
// it may be a shared term that never gets asserted
// result is just Null
Assert(d_bv->isSharedTerm(var));
} else {
- result = d_modelValues[repr];
+ result = d_modelValues[repr];
}
- Debug("bitvector-model") << " => " << result <<"\n";
- return result;
+ Debug("bitvector-model") << " => " << result <<"\n";
+ return result;
}
CoreSolver::Statistics::Statistics()
namespace theory {
namespace bv {
-class Slicer;
-class Base;
+class Slicer;
+class Base;
/**
* Bitvector equality solver
*/
class CoreSolver : public SubtheorySolver {
typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue;
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
struct Statistics {
IntStat d_numCallstoCheck;
Statistics();
- ~Statistics();
- };
-
+ ~Statistics();
+ };
+
// NotifyClass: handles call-back from congruence closure module
class NotifyClass : public eq::EqualityEngineNotify {
CoreSolver& d_solver;
/** The notify class for d_equalityEngine */
NotifyClass d_notify;
-
+
/** Equality engine */
eq::EqualityEngine d_equalityEngine;
/** Store a propagation to the bv solver */
bool storePropagation(TNode literal);
-
+
/** Store a conflict from merging two constants */
void conflict(TNode a, TNode b);
/** To make sure we keep the explanations */
context::CDHashSet<Node, NodeHashFunction> d_reasons;
ModelValue d_modelValues;
- void buildModel();
- bool assertFactToEqualityEngine(TNode fact, TNode reason);
+ void buildModel();
+ bool assertFactToEqualityEngine(TNode fact, TNode reason);
bool decomposeFact(TNode fact);
Node getBaseDecomposition(TNode a);
- Statistics d_statistics;
-public:
+ Statistics d_statistics;
+public:
CoreSolver(context::Context* c, TheoryBV* bv);
~CoreSolver();
bool isComplete() { return d_isCoreTheory; }
void preRegister(TNode node);
bool check(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions);
- void collectModelInfo(TheoryModel* m);
- Node getModelValue(TNode var);
+ void collectModelInfo(TheoryModel* m, bool fullModel);
+ Node getModelValue(TNode var);
void addSharedTerm(TNode t) {
d_equalityEngine.addTriggerTerm(t, THEORY_BV);
}
bool InequalitySolver::check(Theory::Effort e) {
Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
++(d_statistics.d_numCallstoCheck);
-
- bool ok = true;
+
+ bool ok = true;
while (!done() && ok) {
TNode fact = get();
- Debug("bv-subtheory-inequality") << " "<< fact <<"\n";
+ Debug("bv-subtheory-inequality") << " "<< fact <<"\n";
if (fact.getKind() == kind::EQUAL) {
TNode a = fact[0];
TNode b = fact[1];
ok = d_inequalityGraph.addInequality(a, b, false, fact);
if (ok)
- ok = d_inequalityGraph.addInequality(b, a, false, fact);
+ ok = d_inequalityGraph.addInequality(b, a, false, fact);
} else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) {
TNode a = fact[0][0];
TNode b = fact[0][1];
}
if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) {
TNode a = fact[0][1];
- TNode b = fact[0][0];
+ TNode b = fact[0][0];
ok = d_inequalityGraph.addInequality(a, b, true, fact);
// propagate
// if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
- // Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b));
+ // Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b));
// d_bv->storePropagation(neq, SUB_INEQUALITY);
// d_explanations[neq] = fact;
// }
} else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULT) {
TNode a = fact[0][1];
- TNode b = fact[0][0];
+ TNode b = fact[0][0];
ok = d_inequalityGraph.addInequality(a, b, false, fact);
} else if (fact.getKind() == kind::BITVECTOR_ULT) {
TNode a = fact[0];
- TNode b = fact[1];
+ TNode b = fact[1];
ok = d_inequalityGraph.addInequality(a, b, true, fact);
// propagate
// if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
- // Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b));
+ // Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b));
// d_bv->storePropagation(neq, SUB_INEQUALITY);
// d_explanations[neq] = fact;
// }
} else if (fact.getKind() == kind::BITVECTOR_ULE) {
TNode a = fact[0];
- TNode b = fact[1];
+ TNode b = fact[1];
ok = d_inequalityGraph.addInequality(a, b, false, fact);
}
}
-
+
if (!ok) {
std::vector<TNode> conflict;
- d_inequalityGraph.getConflict(conflict);
+ d_inequalityGraph.getConflict(conflict);
d_bv->setConflict(utils::flattenAnd(conflict));
- return false;
+ return false;
}
if (isComplete() && Theory::fullEffort(e)) {
std::vector<Node> lemmas;
d_inequalityGraph.checkDisequalities(lemmas);
for(unsigned i = 0; i < lemmas.size(); ++i) {
- d_bv->lemma(lemmas[i]);
+ d_bv->lemma(lemmas[i]);
}
}
- return true;
+ return true;
}
EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b) {
if (!isComplete())
return EQUALITY_UNKNOWN;
-
+
Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b);
Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a);
// if an inequality containing the terms has been asserted then we know
// the equality is false
if (d_assertionSet.contains(a_lt_b) || d_assertionSet.contains(b_lt_a)) {
- return EQUALITY_FALSE;
+ return EQUALITY_FALSE;
}
-
+
if (!d_inequalityGraph.hasValueInModel(a) ||
!d_inequalityGraph.hasValueInModel(b)) {
- return EQUALITY_UNKNOWN;
+ return EQUALITY_UNKNOWN;
}
// TODO: check if this disequality is entailed by inequalities via transitivity
-
+
BitVector a_val = d_inequalityGraph.getValueInModel(a);
BitVector b_val = d_inequalityGraph.getValueInModel(b);
-
+
if (a_val == b_val) {
- return EQUALITY_TRUE_IN_MODEL;
+ return EQUALITY_TRUE_IN_MODEL;
} else {
- return EQUALITY_FALSE_IN_MODEL;
+ return EQUALITY_FALSE_IN_MODEL;
}
}
d_assertionQueue.push_back(fact);
d_assertionSet.insert(fact);
if (!isInequalityOnly(fact)) {
- d_isComplete = false;
+ d_isComplete = false;
}
}
bool InequalitySolver::isInequalityOnly(TNode node) {
if (d_ineqTermCache.find(node) != d_ineqTermCache.end()) {
- return d_ineqTermCache[node];
+ return d_ineqTermCache[node];
}
-
+
if (node.getKind() == kind::NOT) {
- node = node[0];
+ node = node[0];
}
-
+
if (node.getKind() != kind::EQUAL &&
node.getKind() != kind::BITVECTOR_ULT &&
node.getKind() != kind::BITVECTOR_ULE &&
node.getKind() != kind::SELECT &&
node.getKind() != kind::STORE &&
node.getMetaKind() != kind::metakind::VARIABLE) {
- return false;
+ return false;
}
- bool res = true;
+ bool res = true;
for (unsigned i = 0; i < node.getNumChildren(); ++i) {
res = res && isInequalityOnly(node[i]);
}
- d_ineqTermCache[node] = res;
- return res;
+ d_ineqTermCache[node] = res;
+ return res;
}
void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
Assert (d_explanations.find(literal) != d_explanations.end());
TNode explanation = d_explanations[literal];
assumptions.push_back(explanation);
- Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n";
+ Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n";
}
void InequalitySolver::propagate(Theory::Effort e) {
- Assert (false);
+ Assert (false);
}
-void InequalitySolver::collectModelInfo(TheoryModel* m) {
- Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n";
+void InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+ Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n";
std::vector<Node> model;
d_inequalityGraph.getAllValuesInModel(model);
for (unsigned i = 0; i < model.size(); ++i) {
- Assert (model[i].getKind() == kind::EQUAL);
- m->assertEquality(model[i][0], model[i][1], true);
+ Assert (model[i].getKind() == kind::EQUAL);
+ m->assertEquality(model[i][0], model[i][1], true);
}
}
Node InequalitySolver::getModelValue(TNode var) {
- Assert (isInequalityOnly(var));
- Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")";
+ Assert (isInequalityOnly(var));
+ Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")";
Assert (isComplete());
- Node result = Node();
+ Node result = Node();
if (!d_inequalityGraph.hasValueInModel(var)) {
Assert (d_bv->isSharedTerm(var));
} else {
BitVector val = d_inequalityGraph.getValueInModel(var);
result = utils::mkConst(val);
}
- Debug("bitvector-model") << " => " << result <<"\n";
- return result;
+ Debug("bitvector-model") << " => " << result <<"\n";
+ return result;
}
InequalitySolver::Statistics::Statistics()
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Algebraic solver.
+ ** \brief Algebraic solver.
**
** Algebraic solver.
**/
struct Statistics {
IntStat d_numCallstoCheck;
Statistics();
- ~Statistics();
- };
+ ~Statistics();
+ };
- context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
+ context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
InequalityGraph d_inequalityGraph;
- context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations;
+ context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations;
context::CDO<bool> d_isComplete;
- __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache;
- bool isInequalityOnly(TNode node);
- Statistics d_statistics;
+ __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache;
+ bool isInequalityOnly(TNode node);
+ Statistics d_statistics;
public:
InequalitySolver(context::Context* c, TheoryBV* bv)
: SubtheorySolver(c, bv),
d_ineqTermCache(),
d_statistics()
{}
-
+
bool check(Theory::Effort e);
- void propagate(Theory::Effort e);
+ void propagate(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions);
bool isComplete() { return d_isComplete; }
- void collectModelInfo(TheoryModel* m);
- Node getModelValue(TNode var);
+ void collectModelInfo(TheoryModel* m, bool fullModel);
+ Node getModelValue(TNode var);
EqualityStatus getEqualityStatus(TNode a, TNode b);
- void assertFact(TNode fact);
-};
+ void assertFact(TNode fact);
+};
}
}
}
-#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
+#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
d_propagatedBy(c)
{
if (options::bvEquality()) {
- SubtheorySolver* core_solver = new CoreSolver(c, this);
+ SubtheorySolver* core_solver = new CoreSolver(c, this);
d_subtheories.push_back(core_solver);
d_subtheoryMap[SUB_CORE] = core_solver;
}
if (options::bitvectorInequalitySolver()) {
- SubtheorySolver* ineq_solver = new InequalitySolver(c, this);
+ SubtheorySolver* ineq_solver = new InequalitySolver(c, this);
d_subtheories.push_back(ineq_solver);
d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
}
-
- SubtheorySolver* bb_solver = new BitblastSolver(c, this);
+
+ SubtheorySolver* bb_solver = new BitblastSolver(c, this);
d_subtheories.push_back(bb_solver);
d_subtheoryMap[SUB_BITBLAST] = bb_solver;
}
TheoryBV::~TheoryBV() {
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
- delete d_subtheories[i];
+ delete d_subtheories[i];
}
}
return;
}
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
- d_subtheories[i]->preRegister(node);
+ d_subtheories[i]->preRegister(node);
}
}
if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) {
TNode urem = fact[0];
TNode result = fact[1];
- TNode divisor = urem[1];
+ TNode divisor = urem[1];
Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor);
Node divisor_eq_0 = mkNode(kind::EQUAL,
divisor,
- mkConst(BitVector(getSize(divisor), 0u)));
+ mkConst(BitVector(getSize(divisor), 0u)));
Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
lemma(split);
}
if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) {
TNode urem = fact[1];
TNode result = fact[0];
- TNode divisor = urem[1];
+ TNode divisor = urem[1];
Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor);
Node divisor_eq_0 = mkNode(kind::EQUAL,
divisor,
- mkConst(BitVector(getSize(divisor), 0u)));
+ mkConst(BitVector(getSize(divisor), 0u)));
Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
lemma(split);
}
}
if (Theory::fullEffort(e)) {
- ++(d_statistics.d_numCallsToCheckFullEffort);
+ ++(d_statistics.d_numCallsToCheckFullEffort);
} else {
- ++(d_statistics.d_numCallsToCheckStandardEffort);
+ ++(d_statistics.d_numCallsToCheckStandardEffort);
}
// if we are already in conflict just return the conflict
if (inConflict()) {
while (!done()) {
TNode fact = get().assertion;
- checkForLemma(fact);
+ checkForLemma(fact);
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
- d_subtheories[i]->assertFact(fact);
+ d_subtheories[i]->assertFact(fact);
}
}
bool ok = true;
bool complete = false;
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
- Assert (!inConflict());
+ Assert (!inConflict());
ok = d_subtheories[i]->check(e);
- complete = d_subtheories[i]->isComplete();
+ complete = d_subtheories[i]->isComplete();
if (!ok) {
// if we are in a conflict no need to check with other theories
Assert (inConflict());
sendConflict();
- return;
+ return;
}
if (complete) {
// if the last subtheory was complete we stop
- return;
+ return;
}
}
}
// Assert (fullModel); // can only query full model
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
if (d_subtheories[i]->isComplete()) {
- d_subtheories[i]->collectModelInfo(m);
- return;
+ d_subtheories[i]->collectModelInfo(m, fullModel);
+ return;
}
}
}
Assert(!inConflict());
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
if (d_subtheories[i]->isComplete()) {
- return d_subtheories[i]->getModelValue(var);
+ return d_subtheories[i]->getModelValue(var);
}
}
- Unreachable();
+ Unreachable();
}
void TheoryBV::propagate(Effort e) {
bool ok = true;
for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
- // temporary fix for incremental bit-blasting
+ // temporary fix for incremental bit-blasting
if (d_valuation.isSatLiteral(literal)) {
Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n";
ok = d_out->propagate(literal);
if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) {
std::vector<Node> equalities;
Slicer::splitEqualities(t, equalities);
- return utils::mkAnd(equalities);
+ return utils::mkAnd(equalities);
}
-
+
return t;
}
void TheoryBV::presolve() {
- Debug("bitvector") << "TheoryBV::presolve" << endl;
+ Debug("bitvector") << "TheoryBV::presolve" << endl;
}
bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
// Safe to ignore this one, subtheory should produce a conflict
return true;
}
-
+
d_propagatedBy[literal] = subtheory;
}
if (options::bitvectorEagerBitblast()) {
return EQUALITY_UNKNOWN;
}
-
+
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
if (status != EQUALITY_UNKNOWN) {
- return status;
+ return status;
}
}
return EQUALITY_UNKNOWN; ;
\r
bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {\r
if (d_et.hasGeneralization(m, c)) {\r
+ Trace("fmc-debug") << "Already has generalization, skip." << std::endl;\r
return false;\r
}\r
int newIndex = (int)d_cond.size();\r
Node op = it->first;\r
TypeNode tno = op.getType();\r
for( unsigned i=0; i<tno.getNumChildren(); i++) {\r
- TypeNode tn = tno[i];\r
- if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){\r
- Node mbn;\r
- if (!fm->d_rep_set.hasType(tn)) {\r
- mbn = fm->getSomeDomainElement(tn);\r
- }else{\r
- mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
- }\r
- Node mbnr = fm->getUsedRepresentative( mbn );\r
- fm->d_model_basis_rep[tn] = mbnr;\r
- Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl;\r
- }\r
+ initializeType( fm, tno[i] );\r
}\r
}\r
//now, make models\r
}\r
}\r
\r
+void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){\r
+ if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){\r
+ Trace("fmc") << "Initialize type " << tn << std::endl;\r
+ Node mbn;\r
+ if (!fm->d_rep_set.hasType(tn)) {\r
+ mbn = fm->getSomeDomainElement(tn);\r
+ }else{\r
+ mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
+ }\r
+ Node mbnr = fm->getUsedRepresentative( mbn );\r
+ fm->d_model_basis_rep[tn] = mbnr;\r
+ Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl;\r
+ }\r
+}\r
+\r
void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {\r
Trace(tr) << "(";\r
for( unsigned j=0; j<n.getNumChildren(); j++) {\r
Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );\r
d_quant_cond[f] = op;\r
}\r
+ //make sure all types are set\r
+ for( unsigned i=0; i<f[0].getNumChildren(); i++ ){\r
+ initializeType( fmfmc, f[0][i].getType() );\r
+ }\r
\r
//model check the quantifier\r
doCheck(fmfmc, f, d_quant_models[f], f[1]);\r
Trace("fmc-debug") << "It is a bounding literal, polarity = " << n.getAttribute(BoundIntLitAttribute()) << std::endl;\r
d.addEntry(fm, mkCondDefault(fm, f), n.getAttribute(BoundIntLitAttribute())==1 ? d_false : d_true );\r
}else if( n.getKind() == kind::BOUND_VARIABLE ){\r
+ Trace("fmc-debug") << "Add default entry..." << std::endl;\r
d.addEntry(fm, mkCondDefault(fm, f), n);\r
}\r
else if( n.getKind() == kind::NOT ){\r
}\r
r = fm->getUsedRepresentative( r );\r
}\r
+ Trace("fmc-debug") << "Add constant entry..." << std::endl;\r
d.addEntry(fm, mkCondDefault(fm, f), r);\r
}\r
else{\r
}\r
}\r
Trace("fmc-debug") << "Simplify the definition..." << std::endl;\r
+ d.debugPrint("fmc-debug", Node::null(), this);\r
d.simplify(this, fm);\r
Trace("fmc-debug") << "Done simplifying" << std::endl;\r
}\r
std::map< Node, Node > d_array_term_cond;\r
std::map<Node, std::map< Node, int > > d_quant_var_id;\r
std::map<Node, std::vector< int > > d_star_insts;\r
+ void initializeType( FirstOrderModelFmc * fm, TypeNode tn );\r
Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);\r
bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);\r
protected:\r
NodeBuilder<> nb(kind::OR);
nb << f << ceLit;
Node lem = nb;
- Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl;
+ Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
d_quantEngine->getOutputChannel().lemma( lem );
addedLemma = true;
}
d_quant_active[n] = active;
if( active ){
Debug("quantifiers") << " Active : " << n;
- quantActive = true;
+ if( !TermDb::hasInstConstAttr(n) ){
+ quantActive = true;
+ }
}else{
Debug("quantifiers") << " NOT active : " << n;
if( d_quantEngine->getValuation().isDecision( cel ) ){
//it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
}else{
d_quant_active[n] = true;
- quantActive = true;
+ if( !TermDb::hasInstConstAttr(n) ){
+ quantActive = true;
+ }
Debug("quantifiers") << " Active : " << n << ", no ce assigned." << std::endl;
}
Debug("quantifiers-relevance") << "Quantifier : " << n << std::endl;
NodeBuilder<> nb(kind::OR);
nb << n[0] << body.notNode();
Node lem = nb;
- Debug("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl;
+ Trace("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl;
d_out->lemma( lem );
d_skolemized[n] = true;
}
projects / cvc5.git / commitdiff