typedef std::vector<T> Bits;
typedef __gnu_cxx::hash_map <Node, Bits, NodeHashFunction> TermDefMap;
typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> ModelCache;
typedef void (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*);
typedef T (*AtomBBStrategy) (TNode, TBitblaster<T>*);
// caches and mappings
- TermDefMap d_termCache;
-
+ TermDefMap d_termCache;
+ ModelCache d_modelCache;
+
void initAtomBBStrategies();
void initTermBBStrategies();
protected:
/// function tables for the various bitblasting strategies indexed by node kind
TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
+ virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
public:
TBitblaster();
virtual ~TBitblaster() {}
virtual bool hasBBAtom(TNode atom) const = 0;
virtual void storeBBAtom(TNode atom, T atom_bb) = 0;
+
bool hasBBTerm(TNode node) const;
void getBBTerm(TNode node, Bits& bits) const;
- void storeBBTerm(TNode term, const Bits& bits);
+ void storeBBTerm(TNode term, const Bits& bits);
+ /**
+ * Return a constant representing the value of a in the model.
+ * If fullModel is true set unconstrained bits to 0. If not return
+ * NullNode() for a fully or partially unconstrained.
+ *
+ */
+ Node getTermModel(TNode node, bool fullModel);
+ void invalidateModelCache();
};
typedef std::vector<Node> Bits;
typedef context::CDList<prop::SatLiteral> AssertionList;
typedef context::CDHashMap<prop::SatLiteral, std::vector<prop::SatLiteral> , prop::SatLiteralHashFunction> ExplanationMap;
-
/** This class gets callbacks from minisat on propagations */
class MinisatNotify : public prop::BVSatSolverInterface::Notify {
prop::CnfStream* d_cnf;
TNodeSet d_bbAtoms;
AbstractionModule* d_abstraction;
bool d_emptyNotify;
+
+ context::CDO<bool> d_satSolverFullModel;
void addAtom(TNode atom);
bool hasValue(TNode a);
+ Node getModelFromSatSolver(TNode a, bool fullModel);
public:
void bbTerm(TNode node, Bits& bits);
void bbAtom(TNode node);
void setAbstraction(AbstractionModule* abs);
theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
- /**
- * Return a constant Node representing the value of a variable
- * in the current model.
- * @param a
- *
- * @return
- */
- Node getVarValue(TNode a, bool fullModel=true);
+
/**
* Adds a constant value for each bit-blasted variable in the model.
*
TNodeSet d_bbAtoms;
TNodeSet d_variables;
- Node getVarValue(TNode a, bool fullModel);
+ Node getModelFromSatSolver(TNode a, bool fullModel);
bool isSharedTerm(TNode node);
public:
bool hasInput(TNode input);
void convertToCnfAndAssert();
void assertToSatSolver(Cnf_Dat_t* pCnf);
-
+ Node getModelFromSatSolver(TNode a, bool fullModel) { Unreachable(); }
public:
AigBitblaster();
~AigBitblaster();
template <class T>
TBitblaster<T>::TBitblaster()
: d_termCache()
+ , d_modelCache()
{
initAtomBBStrategies();
initTermBBStrategies();
d_termCache.insert(std::make_pair(node, bits));
}
+template <class T>
+void TBitblaster<T>::invalidateModelCache() {
+ d_modelCache.clear();
+}
+
+template <class T>
+Node TBitblaster<T>::getTermModel(TNode node, bool fullModel) {
+ if (d_modelCache.find(node) != d_modelCache.end())
+ return d_modelCache[node];
+
+ if (node.isConst())
+ return node;
+
+ Node value = getModelFromSatSolver(node, false);
+ if (!value.isNull()) {
+ Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from SatSolver" << node <<" => " << value <<"\n";
+ d_modelCache[node] = value;
+ Assert (value.isConst());
+ return value;
+ }
+
+ if (Theory::isLeafOf(node, theory::THEORY_BV)) {
+ // if it is a leaf may ask for fullModel
+ value = getModelFromSatSolver(node, fullModel);
+ Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from VarValue" << node <<" => " << value <<"\n";
+ Assert (!value.isNull());
+ d_modelCache[node] = value;
+ return value;
+ }
+ Assert (node.getType().isBitVector());
+
+ NodeBuilder<> nb(node.getKind());
+ if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ nb << node.getOperator();
+ }
+
+ for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+ nb << getTermModel(node[i], fullModel);
+ }
+ value = nb;
+ value = Rewriter::rewrite(value);
+ Assert (value.isConst());
+ d_modelCache[node] = value;
+ Debug("bv-term-model")<< "TLazyBitblaster::getTermModel Building Value" << node <<" => " << value <<"\n";
+ return value;
+}
+
} /* bv namespace */
}
Node BVQuickCheck::getVarValue(TNode var) {
- return d_bitblaster->getVarValue(var);
+ return d_bitblaster->getTermModel(var, true);
}
// don't bit-blast lemma atoms
continue;
}
+ Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n";
d_bitblaster->bbAtom(atom);
}
}
Node BitblastSolver::getModelValue(TNode node)
{
- if (!d_validModelCache) {
- d_modelCache.clear();
- d_validModelCache = true;
- }
- return getModelValueRec(node);
-}
-
-Node BitblastSolver::getModelValueRec(TNode node)
-{
- Node val;
- if (node.isConst()) {
- return node;
- }
- NodeMap::iterator it = d_modelCache.find(node);
- if (it != d_modelCache.end()) {
- val = (*it).second;
- Debug("bitvector-model") << node << " => (cached) " << val <<"\n";
- return val;
- }
- if (d_bv->isLeaf(node)) {
- val = d_bitblaster->getVarValue(node);
- if (val == Node()) {
- // If no value in model, just set to 0
- val = utils::mkConst(utils::getSize(node), (unsigned)0);
- }
- } else {
- NodeBuilder<> valBuilder(node.getKind());
- if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
- valBuilder << node.getOperator();
- }
- for (unsigned i = 0; i < node.getNumChildren(); ++i) {
- valBuilder << getModelValueRec(node[i]);
- }
- val = valBuilder;
- val = Rewriter::rewrite(val);
- }
- Assert(val.isConst());
- d_modelCache[node] = val;
- Debug("bitvector-model") << node << " => " << val <<"\n";
+ Node val = d_bitblaster->getTermModel(node, false);
return val;
}
+// Node BitblastSolver::getModelValueRec(TNode node)
+// {
+// Node val;
+// if (node.isConst()) {
+// return node;
+// }
+// NodeMap::iterator it = d_modelCache.find(node);
+// if (it != d_modelCache.end()) {
+// val = (*it).second;
+// Debug("bitvector-model") << node << " => (cached) " << val <<"\n";
+// return val;
+// }
+// if (d_bv->isLeaf(node)) {
+// val = d_bitblaster->getVarValue(node);
+// if (val == Node()) {
+// // If no value in model, just set to 0
+// val = utils::mkConst(utils::getSize(node), (unsigned)0);
+// }
+// } else {
+// NodeBuilder<> valBuilder(node.getKind());
+// if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+// valBuilder << node.getOperator();
+// }
+// for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+// valBuilder << getModelValueRec(node[i]);
+// }
+// val = valBuilder;
+// val = Rewriter::rewrite(val);
+// }
+// Assert(val.isConst());
+// d_modelCache[node] = val;
+// Debug("bitvector-model") << node << " => " << val <<"\n";
+// return val;
+// }
+
void BitblastSolver::setConflict(TNode conflict) {
Node final_conflict = conflict;
AbstractionModule* d_abstractionModule;
BVQuickCheck* d_quickCheck;
QuickXPlain* d_quickXplain;
- Node getModelValueRec(TNode node);
+ // Node getModelValueRec(TNode node);
void setConflict(TNode conflict);
public:
BitblastSolver(context::Context* c, TheoryBV* bv);
*
* @return
*/
-Node EagerBitblaster::getVarValue(TNode a, bool fullModel) {
+Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
if (!hasBBTerm(a)) {
- Assert(isSharedTerm(a));
- return Node();
+ return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node();
}
+
Bits bits;
getBBTerm(a, bits);
Integer value(0);
bit_value = d_satSolver->value(bit);
Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
} else {
- // the bit is unconstrainted so we can give it an arbitrary value
+ if (!fullModel) return Node();
+ // unconstrained bits default to false
bit_value = prop::SAT_VALUE_FALSE;
}
Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
- TNodeSet::const_iterator it = d_variables.begin();
+ TNodeSet::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, fullModel);
- if(const_value == Node()) {
- if( fullModel ){
- // if the value is unassigned just set it to zero
- const_value = utils::mkConst(BitVector(utils::getSize(var), 0u));
- }
- }
+ if (d_bv->isLeaf(var) || isSharedTerm(var)) {
+ // only shared terms could not have been bit-blasted
+ Assert (hasBBTerm(var) || isSharedTerm(var));
+
+ Node const_value = getModelFromSatSolver(var, fullModel);
+
if(const_value != Node()) {
- Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
+ Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= "
<< var << " "
<< const_value << "))\n";
m->assertEquality(var, const_value, true);
, d_bbAtoms()
, d_abstraction(NULL)
, d_emptyNotify(emptyNotify)
+ , d_satSolverFullModel(c, false)
, d_name(name)
, d_statistics(name) {
d_satSolver = prop::SatSolverFactory::createMinisat(c, name);
}
}
Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n";
+ d_satSolverFullModel.set(true);
return prop::SAT_VALUE_TRUE == d_satSolver->solve();
}
d_bv->d_out->safePoint();
}
+
EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) {
+ Debug("bv-equality-status")<< "TLazyBitblaster::getEqualityStatus " << a <<" = " << b <<"\n";
+ Debug("bv-equality-status")<< "BVSatSolver has full model? " << d_satSolverFullModel.get() <<"\n";
- // We don't want to bit-blast every possibly expensive term for the sake of equality checking
- if (hasBBTerm(a) && hasBBTerm(b)) {
-
- Bits a_bits, b_bits;
- getBBTerm(a, a_bits);
- getBBTerm(b, b_bits);
- theory::EqualityStatus status = theory::EQUALITY_TRUE_IN_MODEL;
- for (unsigned i = 0; i < a_bits.size(); ++ i) {
- if (d_cnfStream->hasLiteral(a_bits[i]) && d_cnfStream->hasLiteral(b_bits[i])) {
- prop::SatLiteral a_lit = d_cnfStream->getLiteral(a_bits[i]);
- prop::SatValue a_lit_value = d_satSolver->value(a_lit);
- if (a_lit_value != prop::SAT_VALUE_UNKNOWN) {
- prop::SatLiteral b_lit = d_cnfStream->getLiteral(b_bits[i]);
- prop::SatValue b_lit_value = d_satSolver->value(b_lit);
- if (b_lit_value != prop::SAT_VALUE_UNKNOWN) {
- if (a_lit_value != b_lit_value) {
- return theory::EQUALITY_FALSE_IN_MODEL;
- }
- } else {
- status = theory::EQUALITY_UNKNOWN;
- }
- } {
- status = theory::EQUALITY_UNKNOWN;
- }
- } else {
- status = theory::EQUALITY_UNKNOWN;
- }
- }
+ // First check if it trivially rewrites to false/true
+ Node a_eq_b = Rewriter::rewrite(utils::mkNode(kind::EQUAL, a, b));
- return status;
+ if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE;
+ if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE;
- } else {
- return theory::EQUALITY_UNKNOWN;
+ if (!d_satSolverFullModel.get())
+ return theory::EQUALITY_UNKNOWN;
+
+ // Check if cache is valid (invalidated in check and pops)
+ if (d_bv->d_invalidateModelCache.get()) {
+ invalidateModelCache();
}
+ d_bv->d_invalidateModelCache.set(false);
+
+ Node a_value = getTermModel(a, true);
+ Node b_value = getTermModel(b, true);
+
+ Assert (a_value.isConst() &&
+ b_value.isConst());
+
+ if (a_value == b_value) {
+ Debug("bv-equality-status")<< "theory::EQUALITY_TRUE_IN_MODEL\n";
+ return theory::EQUALITY_TRUE_IN_MODEL;
+ }
+ Debug("bv-equality-status")<< "theory::EQUALITY_FALSE_IN_MODEL\n";
+ return theory::EQUALITY_FALSE_IN_MODEL;
}
*
* @return
*/
-Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) {
+Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
if (!hasBBTerm(a)) {
- Assert(isSharedTerm(a));
- return Node();
+ return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node();
}
+
Bits bits;
getBBTerm(a, bits);
Integer value(0);
bit_value = d_satSolver->value(bit);
Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
} else {
- // the bit is unconstrainted so we can give it an arbitrary value
+ if (!fullModel) return Node();
+ // unconstrained bits default to false
bit_value = prop::SAT_VALUE_FALSE;
}
Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
}
void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
- TNodeSet::iterator it = d_variables.begin();
- for (; it!= d_variables.end(); ++it) {
+ std::set<Node> termSet;
+ d_bv->computeRelevantTerms(termSet);
+
+ for (std::set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) {
TNode var = *it;
- if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) {
- Node const_value = getVarValue(var, fullModel);
- if(const_value == Node()) {
- 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") << "TLazyBitblaster::collectModelInfo (assert (= "
- << var << " "
- << const_value << "))\n";
+ // not actually a leaf of the bit-vector theory
+ if (d_variables.find(var) == d_variables.end())
+ continue;
+
+ Assert (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var));
+ // only shared terms could not have been bit-blasted
+ Assert (hasBBTerm(var) || isSharedTerm(var));
+
+ Node const_value = getModelFromSatSolver(var, fullModel);
+ Assert (const_value.isNull() || const_value.isConst());
+ if(const_value != Node()) {
+ Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
+ << var << " "
+ << const_value << "))\n";
m->assertEquality(var, const_value, true);
- }
}
}
}
d_bbAtoms.clear();
d_variables.clear();
d_termCache.clear();
-
+
// recreate sat solver
d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx);
d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
d_staticLearnCache(),
d_lemmasAdded(c, false),
d_conflict(c, false),
+ d_invalidateModelCache(c, true),
d_literalsToPropagate(c),
d_literalsToPropagateIndex(c, 0),
d_propagatedBy(c),
void TheoryBV::check(Effort e)
{
Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
-
+ // we may be getting new assertions so the model cache may not be sound
+ d_invalidateModelCache.set(true);
// if we are using the eager solver
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
// this can only happen on an empty benchmark
// Are we in conflict?
context::CDO<bool> d_conflict;
+ // Invalidate the model cache if check was called
+ context::CDO<bool> d_invalidateModelCache;
+
/** The conflict node */
Node d_conflictNode;
projects / cvc5.git / commitdiff