libprop_la_SOURCES = \
prop_engine.cpp \
prop_engine.h \
- sat.h
+ sat.h \
+ cnf_stream.h \
+ cnf_stream.cpp \
+ cnf_conversion.h
SUBDIRS = minisat
--- /dev/null
+/********************* -*- C++ -*- */
+/** cnf_conversion.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** A type for describing possible CNF conversions.
+ **/
+
+#ifndef __CVC4__CNF_CONVERSION_H
+#define __CVC4__CNF_CONVERSION_H
+
+namespace CVC4 {
+
+enum CnfConversion {
+ CNF_DIRECT_EXPONENTIAL = 0,
+ CNF_VAR_INTRODUCTION = 1
+};
+
+inline std::ostream& operator<<(std::ostream&, CVC4::CnfConversion) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out, CVC4::CnfConversion c) {
+ using namespace CVC4;
+
+ switch(c) {
+ case CNF_DIRECT_EXPONENTIAL:
+ out << "CNF_DIRECT_EXPONENTIAL";
+ break;
+ case CNF_VAR_INTRODUCTION:
+ out << "CNF_VAR_INTRODUCTION";
+ break;
+ default:
+ out << "UNKNOWN-CONVERTER!" << int(c);
+ }
+
+ return out;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CNF_CONVERSION_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** cnf_stream.cpp
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** A CNF converter that takes in asserts and has the side effect
+ ** of given an equisatisfiable stream of assertions to PropEngine.
+ **/
+
+#include "prop/cnf_stream.h"
+#include "prop/prop_engine.h"
+#include "expr/node.h"
+#include "util/Assert.h"
+
+#include <queue>
+
+using namespace CVC4::prop::minisat;
+using namespace std;
+
+
+namespace CVC4 {
+namespace prop {
+
+CnfStream::CnfStream(PropEngine *pe) :
+ d_propEngine(pe){}
+
+TseitinCnfStream::TseitinCnfStream(PropEngine *pe):
+ CnfStream(pe){}
+
+
+void CnfStream::insertClauseIntoStream(vec<Lit> & c){
+ d_propEngine->assertClause(c);
+}
+
+void CnfStream::insertClauseIntoStream(minisat::Lit a){
+ vec<Lit> clause(1);
+ clause[0] = a;
+ insertClauseIntoStream(clause);
+}
+void CnfStream::insertClauseIntoStream(minisat::Lit a,minisat::Lit b){
+ vec<Lit> clause(2);
+ clause[0] = a;
+ clause[1] = b;
+ insertClauseIntoStream(clause);
+}
+void CnfStream::insertClauseIntoStream(minisat::Lit a,minisat::Lit b, minisat::Lit c){
+ vec<Lit> clause(3);
+ clause[0] = a;
+ clause[1] = b;
+ clause[2] = c;
+ insertClauseIntoStream(clause);
+}
+
+bool CnfStream::isCached(const Node & n) const {
+ return d_translationCache.find(n) != d_translationCache.end();
+}
+
+Lit CnfStream::lookupInCache(const Node & n) const {
+ Assert(isCached(n));
+ return d_translationCache.find(n)->second;
+}
+
+void CnfStream::flushCache(){
+ d_translationCache.clear();
+}
+
+void CnfStream::registerMapping(const Node & node, Lit lit, bool atom){
+ //Prop engine does not need to know this mapping
+ d_translationCache.insert(make_pair(node,lit));
+ if(atom)
+ d_propEngine->registerAtom(node, lit);
+}
+
+Lit CnfStream::acquireFreshLit(const Node & n){
+ return d_propEngine->requestFreshLit();
+}
+
+Lit CnfStream::aquireAndRegister(const Node & node, bool atom){
+ Lit l = acquireFreshLit(node);
+ registerMapping(node, l, atom);
+ return l;
+}
+
+/***********************************************/
+/***********************************************/
+/************ End of CnfStream *****************/
+/***********************************************/
+/***********************************************/
+
+Lit TseitinCnfStream::handleAtom(const Node & n){
+ Lit l = aquireAndRegister(n, true);
+ switch(n.getKind()){ /* TRUE and FALSE are handled specially. */
+ case TRUE:
+ insertClauseIntoStream( l );
+ break;
+ case FALSE:
+ insertClauseIntoStream( ~l );
+ break;
+ default: //Does nothing else
+ break;
+ }
+ return l;
+}
+
+Lit TseitinCnfStream::handleXor(const Node & n){
+ // n: a XOR b
+
+ Lit a = recTransform(n[0]);
+ Lit b = recTransform(n[1]);
+
+ Lit l = aquireAndRegister(n);
+
+ insertClauseIntoStream( a, b, ~l);
+ insertClauseIntoStream( a, ~b, l);
+ insertClauseIntoStream(~a, b, l);
+ insertClauseIntoStream(~a, ~b, ~l);
+
+ return l;
+}
+
+ /* For a small efficiency boost target needs to already be allocated to have
+ size of the number of children of n.
+ */
+void TseitinCnfStream::mapRecTransformOverChildren(const Node& n, vec<Lit> & target){
+ Assert(target.size() == n.getNumChildren());
+
+ int i = 0;
+ Node::iterator subExprIter = n.begin();
+
+ while(subExprIter != n.end()){
+ Lit equivalentLit = recTransform(*subExprIter);
+ target[i] = equivalentLit;
+ ++subExprIter; ++i;
+ }
+}
+
+Lit TseitinCnfStream::handleOr(const Node& n){
+ //child_literals
+ vec<Lit> lits(n.getNumChildren());
+ mapRecTransformOverChildren(n, lits);
+
+ Lit e = aquireAndRegister(n);
+
+ /* e <-> (a1 | a2 | a3 | ...)
+ *: e -> (a1 | a2 | a3 | ...)
+ * : ~e | (
+ * : ~e | a1 | a2 | a3 | ...
+ * e <- (a1 | a2 | a3 | ...)
+ * : e <- (a1 | a2 | a3 |...)
+ * : e | ~(a1 | a2 | a3 |...)
+ * :
+ * : (e | ~a1) & (e |~a2) & (e & ~a3) & ...
+ */
+
+ vec<Lit> c;
+ c.push(~e);
+
+ for( int index = 0; index < lits.size(); ++index){
+ Lit a = lits[index];
+ c.push(a);
+ insertClauseIntoStream( e, ~a);
+ }
+ insertClauseIntoStream(c);
+
+ return e;
+}
+
+
+/* TODO: this only supports 2-ary <=> nodes atm.
+ * Should this be changed?
+ */
+Lit TseitinCnfStream::handleIff(const Node& n){
+ Assert(n.getKind() == IFF);
+ Assert(n.getNumChildren() == 2);
+ // n: a <=> b;
+
+ Lit a = recTransform(n[0]);
+ Lit b = recTransform(n[1]);
+
+ Lit l = aquireAndRegister(n);
+
+ /* l <-> (a<->b)
+ * : l -> ((a-> b) & (b->a))
+ * : ~l | ((~a | b) & (~b |a))
+ * : (~a | b | ~l ) & (~b | a | ~l)
+ *
+ * : (a<->b) -> l
+ * : ~((a & b) | (~a & ~b)) | l
+ * : (~(a & b)) & (~(~a & ~b)) | l
+ * : ((~a | ~b) & (a | b)) | l
+ * : (~a | ~b | l) & (a | b | l)
+ */
+
+ insertClauseIntoStream( ~a, b,~l);
+ insertClauseIntoStream( a,~b,~l);
+ insertClauseIntoStream( ~a,~b, l);
+ insertClauseIntoStream( a, b, l);
+
+ return l;
+}
+
+Lit TseitinCnfStream::handleAnd(const Node& n){
+ //TODO: we know the exact size of the this.
+ //Dynamically allocated array would have less overhead no?
+ vec<Lit> lits(n.getNumChildren());
+ mapRecTransformOverChildren(n, lits);
+
+ Lit e = aquireAndRegister(n);
+
+ /* e <-> (a1 & a2 & a3 & ...)
+ * : e -> (a1 & a2 & a3 & ...)
+ * : ~e | (a1 & a2 & a3 & ...)
+ * : (~e | a1) & (~e | a2) & ...
+ * e <- (a1 & a2 & a3 & ...)
+ * : e <- (a1 & a2 & a3 & ...)
+ * : e | ~(a1 & a2 & a3 & ...)
+ * : e | (~a1 | ~a2 | ~a3 | ...)
+ * : e | ~a1 | ~a2 | ~a3 | ...
+ */
+
+ vec<Lit> c;
+ c.push(e);
+ for(int index = 0; index < lits.size(); ++index){
+ Lit a = lits[index];
+ c.push(~a);
+ insertClauseIntoStream( ~e, a );
+ }
+ insertClauseIntoStream(c);
+
+ return e;
+}
+
+Lit TseitinCnfStream::handleImplies(const Node & n){
+ Assert(n.getKind() == IMPLIES);
+ // n: a => b;
+
+ Lit a = recTransform(n[0]);
+ Lit b = recTransform(n[1]);
+
+ Lit l = aquireAndRegister(n);
+
+ /* l <-> (a->b)
+ * (l -> (a->b)) & (l <- (a->b))
+ * : l -> (a -> b)
+ * : ~l | (~ a | b)
+ * : (~l | ~a | b)
+ * (~l | ~a | b) & (l<- (a->b))
+ * : (a->b) -> l
+ * : ~(~a | b) | l
+ * : (a & ~b) | l
+ * : (a | l) & (~b | l)
+ * (~l | ~a | b) & (a | l) & (~b | l)
+ */
+
+ insertClauseIntoStream( a, l);
+ insertClauseIntoStream( ~b, l);
+ insertClauseIntoStream( ~l, ~a, b);
+
+ return l;
+}
+
+Lit TseitinCnfStream::handleNot(const Node & n){
+ Assert(n.getKind() == NOT);
+
+ // n : NOT m
+ Node m = n[0];
+ Lit equivM = recTransform(m);
+
+ registerMapping(n, ~equivM, false);
+
+ return equivM;
+}
+
+//FIXME: This function is a major hack! Should be changed ASAP
+//Assumes binary no else if branchs, and that ITEs
+Lit TseitinCnfStream::handleIte(const Node & n){
+ Assert(n.getKind() == ITE);
+
+ // n : IF c THEN t ELSE f ENDIF;
+ Lit c = recTransform(n[0]);
+ Lit t = recTransform(n[1]);
+ Lit f = recTransform(n[2]);
+
+ // d <-> IF c THEN tB ELSE fb
+ // : d -> (c & tB) | (~c & fB)
+ // : ~d | ( (c & tB) | (~c & fB) )
+ // : x | (y & z) = (x | y) & (x | z)
+ // : ~d | ( ((c & t) | ~c ) & ((c & t) | f ) )
+ // : ~d | ( (((c | ~c) & (~c | t))) & ((c | f) & (f | t)) )
+ // : ~d | ( (~c | t) & (c | f) & (f | t) )
+ // : (~d | ~c | t) & (~d | c | f) & (~d | f | t)
+
+ // : ~d | (c & t & f)
+ // : (~d | c) & (~d | t) & (~d | f)
+ // ( IF c THEN tB ELSE fb) -> d
+ // :~((c & tB) | (~c & fB)) | d
+ // : ((~c | ~t)& ( c |~fb)) | d
+ // : (~c | ~ t | d) & (c | ~f | d)
+
+ Lit d = aquireAndRegister(n);
+
+ insertClauseIntoStream(~d , ~c , t);
+ insertClauseIntoStream(~d , c , f);
+ insertClauseIntoStream(~d , f , t);
+ insertClauseIntoStream(~c , ~t , d);
+ insertClauseIntoStream( c , ~f , d);
+
+ return d;
+}
+
+//FIXME: This function is a major hack! Should be changed ASAP
+//TODO: Should be moved. Not sure where...
+//TODO: Should use positive defintion, i.e. what kinds are atomic.
+bool atomic(const Node & n){
+ switch(n.getKind()){
+ case NOT:
+ case XOR:
+ case ITE:
+ case IFF:
+ case OR:
+ case AND:
+ return false;
+ default:
+ return true;
+ }
+}
+
+//TODO: The following code assumes everthing is either
+// an atom or is a logical connective. This ignores quantifiers and lambdas.
+Lit TseitinCnfStream::recTransform(const Node & n){
+ if(isCached(n)){
+ return lookupInCache(n);
+ }
+
+ if(atomic(n)){
+ return handleAtom(n);
+ }else{
+ //Assume n is a logical connective
+ switch(n.getKind()){
+ case NOT:
+ return handleNot(n);
+ case XOR:
+ return handleXor(n);
+ case ITE:
+ return handleIte(n);
+ case IFF:
+ return handleIff(n);
+ case OR:
+ return handleOr(n);
+ case AND:
+ return handleAnd(n);
+ default:
+ Unreachable();
+ }
+ }
+}
+
+void TseitinCnfStream::convertAndAssert(const Node & n){
+ //n has already been mapped so use the previous result
+ if(isCached(n)){
+ Lit l = lookupInCache(n);
+ insertClauseIntoStream(l);
+ return;
+ }
+
+ Lit e = recTransform(n);
+ insertClauseIntoStream( e );
+
+ //I've commented the following section out because it uses a bit too much intelligence.
+
+ /*
+ if(n.getKind() == AND){
+ // this code is required to efficiently flatten and
+ // assert each part of the node.
+ // This would be rendered unnessecary if the input was given differently
+ queue<Node> and_queue;
+ and_queue.push(n);
+
+ //This was changed to use a queue due to pressure on the C stack.
+
+ //TODO: this does no cacheing of what has been asserted.
+ //Low hanging fruit
+ while(!and_queue.empty()){
+ Node curr = and_queue.front();
+ and_queue.pop();
+ if(curr.getKind() == AND){
+ for(Node::iterator i = curr.begin(); i != curr.end(); ++i){
+ and_queue.push(*i);
+ }
+ }else{
+ convertAndAssert(curr);
+ }
+ }
+ }else if(n.getKind() == OR){
+ //This is special cased so minimal translation is done for things that
+ //are already in CNF so minimal work is done on clauses.
+ vec<Lit> c;
+ for(Node::iterator i = n.begin(); i != n.end(); ++i){
+ Lit cl = recTransform(*i);
+ c.push(cl);
+ }
+ insertClauseIntoStream(c);
+ }else{
+ Lit e = recTransform(n);
+ insertClauseIntoStream( e );
+ }
+ */
+}
+
+
+
+
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* -*- C++ -*- */
+/** cnf_stream.h
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** This class takes a sequence of formulas.
+ ** It outputs a stream of clauses that is propositional
+ ** equisatisfiable with the conjunction of the formulas.
+ ** This stream is maintained in an online fashion.
+ **
+ ** Unlike other parts of the system it is aware of the PropEngine's
+ ** internals such as the representation and translation of
+ **/
+
+
+#ifndef __CVC4__CNF_STREAM_H
+#define __CVC4__CNF_STREAM_H
+
+//TODO: Why am i including this? Who knows...
+#include "cvc4_config.h"
+
+#include "expr/node.h"
+#include "prop/minisat/simp/SimpSolver.h"
+#include "prop/minisat/core/SolverTypes.h"
+#include "prop/prop_engine.h"
+
+#include <map>
+
+namespace CVC4 {
+ class PropEngine;
+}
+
+
+namespace CVC4 {
+namespace prop {
+
+class CnfStream {
+
+private:
+ /**
+ * d_propEngine is the PropEngine that the CnfStream interacts with directly through
+ * the follwoing functions:
+ * - insertClauseIntoStream
+ * - acquireFreshLit
+ * - registerMapping
+ */
+ PropEngine *d_propEngine;
+
+ /**Cache of what literal have been registered to a node.
+ *Not strictly needed for correctness.
+ *This can be flushed when memory is under pressure.
+ */
+ std::map<Node,minisat::Lit> d_translationCache;
+
+protected:
+
+ /**
+ * Uniform interface for sending a clause back to d_propEngine.
+ * May want to have internal datastructures later on
+ */
+ void insertClauseIntoStream(minisat::vec<minisat::Lit> & c);
+ void insertClauseIntoStream(minisat::Lit a);
+ void insertClauseIntoStream(minisat::Lit a,minisat::Lit b);
+ void insertClauseIntoStream(minisat::Lit a,minisat::Lit b, minisat::Lit c);
+
+
+ //utilities for the translation cache;
+ bool isCached(const Node & n) const;
+ minisat::Lit lookupInCache(const Node & n) const;
+
+ /**
+ * Empties the internal translation cache.
+ */
+ void flushCache();
+
+ //negotiates the mapping of atoms to literals with PropEngine
+ void registerMapping(const Node & node, minisat::Lit lit, bool atom = false);
+ minisat::Lit acquireFreshLit(const Node & n);
+ minisat::Lit aquireAndRegister(const Node & n, bool atom = false);
+
+public:
+ /**
+ * Constructs a CnfStream that sends constructs an equisatisfiable set of clauses
+ * and sends them to pe.
+ */
+ CnfStream(CVC4::PropEngine *pe);
+
+
+ /**
+ * Converts and asserts a formula.
+ * @param n node to convert and assert
+ */
+ virtual void convertAndAssert(const Node & n) = 0;
+
+}; /* class CnfStream */
+
+
+/**
+ * TseitinCnfStream is based on the following recursive algorithm
+ * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
+ * The general gist of the algorithm is to introduce a new literal that
+ * will be equivalent to each subexpression in the constructed equisatisfiable formula
+ * then subsistute the new literal for the formula, and to do this recursively.
+ *
+ * This implementation does this in a single recursive pass.
+ */
+class TseitinCnfStream : public CnfStream {
+
+public:
+ void convertAndAssert(const Node & n);
+ TseitinCnfStream(CVC4::PropEngine *pe);
+
+private:
+
+ /* Each of these formulas handles takes care of a Node of each Kind.
+ *
+ * Each handleX(Node &n) is responsibile for:
+ * - constructing a new literal, l (if nessecary)
+ * - calling registerNode(n,l)
+ * - adding clauses asure that l is equivalent to the Node
+ * - calling recTransform on its children (if nessecary)
+ * - returning l
+ *
+ * handleX( n ) can assume that n is not in d_translationCache
+ */
+ minisat::Lit handleAtom(const Node & n);
+ minisat::Lit handleNot(const Node & n);
+ minisat::Lit handleXor(const Node & n);
+ minisat::Lit handleImplies(const Node & n);
+ minisat::Lit handleIff(const Node & n);
+ minisat::Lit handleIte(const Node & n);
+
+ minisat::Lit handleAnd(const Node& n);
+ minisat::Lit handleOr(const Node& n);
+
+
+ /**
+ *Maps recTransform over the children of a node.
+ *This is very useful for n-ary Kinds (OR, AND).
+ *
+ *Non n-ary kinds (IMPLIES) should avoid using this as it requires a
+ *tiny bit of extra overhead, and it leads to less readable code.
+ *
+ * precondition: target.size() == n.getNumChildren()
+ */
+ void mapRecTransformOverChildren(const Node& n, minisat::vec<minisat::Lit> & target);
+
+ //Recurisively dispatches the various Kinds to the appropriate handler.
+ minisat::Lit recTransform(const Node & n);
+
+}; /* class TseitinCnfStream */
+
+}/* prop namespace */
+}/* CVC4 namespace */
+
+
+
+#endif /* __CVC4__CNF_STREAM_H */
**/
#include "prop/prop_engine.h"
+#include "prop/cnf_stream.h"
+
#include "theory/theory_engine.h"
#include "util/decision_engine.h"
#include "prop/minisat/mtl/Vec.h"
namespace CVC4 {
PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) :
- d_de(de), d_te(te) {
+ d_de(de),
+ d_te(te){
+ d_cnfStream = new CVC4::prop::TseitinCnfStream(this);
+}
+
+PropEngine::~PropEngine(){
+ delete d_cnfStream;
+}
+
+
+void PropEngine::assertClause(vec<Lit> & c){
+ /*we can also here add a context dependent queue of assertions
+ *for restarting the sat solver
+ */
+ //TODO assert that each lit has been mapped to an atom or requested
+ d_sat.addClause(c);
}
-void PropEngine::addVars(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>* varsReverse, Node e) {
- Debug("prop") << "adding vars to " << e << endl;
- for(Node::iterator i = e.begin(); i != e.end(); ++i) {
- Debug("prop") << "expr " << *i << endl;
- if((*i).getKind() == VARIABLE) {
- if(vars->find(*i) == vars->end()) {
- Var v = minisat->newVar();
- Debug("prop") << "adding var " << *i << " <--> " << v << endl;
- (*vars).insert(make_pair(*i, v));
- (*varsReverse).insert(make_pair(v, *i));
- } else Debug("prop") << "using var " << *i << " <--> " << (*vars)[*i] << endl;
- } else addVars(minisat, vars, varsReverse, *i);
- }
+void PropEngine::registerAtom(const Node & n, Lit l){
+ d_atom2lit.insert(make_pair(n,l));
+ d_lit2atom.insert(make_pair(l,n));
}
-static void doAtom(SimpSolver* minisat, map<Node, Var>* vars, Node e, vec<Lit>* c) {
- if(e.getKind() == VARIABLE) {
- map<Node, Var>::iterator v = vars->find(e);
- Assert(v != vars->end());
- c->push(Lit(v->second, false));
- return;
- }
- if(e.getKind() == NOT) {
- Assert(e.getNumChildren() == 1);
- Node child = *e.begin();
- Assert(child.getKind() == VARIABLE);
- map<Node, Var>::iterator v = vars->find(child);
- Assert(v != vars->end());
- c->push(Lit(v->second, true));
- return;
- }
- if(e.getKind() == OR) {
- for(Node::iterator i = e.begin(); i != e.end(); ++i) {
- doAtom(minisat, vars, *i, c);
- }
- return;
- }
- Unhandled(e.getKind());
+Lit PropEngine::requestFreshLit(){
+ Var v = d_sat.newVar();
+ Lit l(v,false);
+ return l;
}
-static void doClause(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>* varsReverse, Node e) {
- vec<Lit> c;
- Debug("prop") << " " << e << endl;
- if(e.getKind() == VARIABLE || e.getKind() == NOT) {
- doAtom(minisat, vars, e, &c);
- } else if(e.getKind() == FALSE) {
- // inconsistency
- Notice() << "adding FALSE clause" << endl;
- Var v = minisat->newVar();
- c.push(Lit(v, true));
- minisat->addClause(c);
- Notice() << "added unit clause " << v << " [[ " << (*varsReverse)[v] << " ]]" << endl;
- c.clear();
- c.push(Lit(v, false));
- minisat->addClause(c);
- Notice() << "added unit clause -" << v << " [[ -" << (*varsReverse)[v] << " ]]" << endl;
- } else if(e.getKind() == TRUE) {
- Notice() << "adding TRUE clause (do nothing)" << endl;
- // do nothing
- } else {
- Assert(e.getKind() == OR);
- for(Node::iterator i = e.begin(); i != e.end(); ++i) {
- Debug("prop") << " " << *i << endl;
- doAtom(minisat, vars, *i, &c);
- }
- }
- Notice() << "added clause of length " << c.size() << endl;
- for(int i = 0; i < c.size(); ++i)
- Notice() << " " << (sign(c[i]) ? "-" : "") << var(c[i]);
- Notice() << " [[";
- for(int i = 0; i < c.size(); ++i)
- Notice() << " " << (sign(c[i]) ? "-" : "") << (*varsReverse)[var(c[i])];
- Notice() << " ]] " << endl;
- minisat->addClause(c);
+void PropEngine::assertFormula(const Node& node) {
+ d_cnfStream->convertAndAssert(node);
}
-void PropEngine::solve(Node e) {
- // FIXME: when context mgr comes online, keep the solver around
- // between solve() calls if we can
- CVC4::prop::minisat::SimpSolver sat;
- std::map<Node, CVC4::prop::minisat::Var> vars;
- std::map<CVC4::prop::minisat::Var, Node> varsReverse;
+void PropEngine::solve() {
- Debug("prop") << "SOLVING " << e << endl;
- addVars(&sat, &vars, &varsReverse, e);
- if(e.getKind() == AND) {
- Debug("prop") << "AND" << endl;
- for(Node::iterator i = e.begin(); i != e.end(); ++i)
- doClause(&sat, &vars, &varsReverse, *i);
- } else doClause(&sat, &vars, &varsReverse, e);
+ //TODO: may need to restart if a previous query returned false
- sat.verbosity = 1;
- bool result = sat.solve();
+ d_sat.verbosity = 1;
+ bool result = d_sat.solve();
Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
- if(result) {
- Notice() << "model:" << endl;
- for(int i = 0; i < sat.model.size(); ++i)
- Notice() << " " << toInt(sat.model[i]);
- Notice() << endl;
- for(int i = 0; i < sat.model.size(); ++i)
- Notice() << " " << varsReverse[i] << " is "
- << (sat.model[i] == l_False ? "FALSE" :
- (sat.model[i] == l_Undef ? "UNDEF" :
- "TRUE")) << endl;
- } else {
- Notice() << "conflict:" << endl;
- for(int i = 0; i < sat.conflict.size(); ++i)
- Notice() << " " << (sign(sat.conflict[i]) ? "-" : "") << var(sat.conflict[i]);
- Notice() << " [[";
- for(int i = 0; i < sat.conflict.size(); ++i)
- Notice() << " " << (sign(sat.conflict[i]) ? "-" : "") << varsReverse[var(sat.conflict[i])];
- Notice() << " ]] " << endl;
- }
}
}/* CVC4 namespace */
#include "prop/minisat/core/SolverTypes.h"
#include <map>
+#include "prop/cnf_stream.h"
+
+namespace CVC4 {
+ namespace prop {
+ class CnfStream;
+ }
+}
namespace CVC4 {
class PropEngine {
DecisionEngine &d_de;
TheoryEngine &d_te;
- //CVC4::prop::minisat::SimpSolver d_sat;
- //std::map<Node, CVC4::prop::minisat::Var> d_vars;
- //std::map<CVC4::prop::minisat::Var, Node> d_varsReverse;
- void addVars(CVC4::prop::minisat::SimpSolver*, std::map<Node, CVC4::prop::minisat::Var>*, std::map<CVC4::prop::minisat::Var, Node>*, Node);
+ friend class CVC4::prop::CnfStream;
+
+ /* Morgan: I added these back.
+ * Why did you push these into solve()?
+ * I am guessing this is for either a technical reason I'm not seeing,
+ * or that you wanted to have a clean restart everytime solve() was called
+ * and to start from scratch everytime. (Avoid push/pop problems?)
+ * Is this right?
+ */
+ CVC4::prop::minisat::SimpSolver d_sat;
+
+
+ std::map<Node, CVC4::prop::minisat::Lit> d_atom2lit;
+ std::map<CVC4::prop::minisat::Lit, Node> d_lit2atom;
+ /**
+ * Adds mapping of n -> l to d_node2lit, and
+ * a mapping of l -> n to d_lit2node.
+ */
+ void registerAtom(const Node & n, CVC4::prop::minisat::Lit l);
+
+
+
+ CVC4::prop::minisat::Lit requestFreshLit();
+ bool isNodeMapped(const Node & n) const;
+ CVC4::prop::minisat::Lit lookupLit(const Node & n) const;
+
+
+ /**
+ * Asserts an internally constructed clause.
+ * Each literal is assumed to be in the 1:1 mapping contained in d_node2lit & d_lit2node.
+ * @param c the clause to be asserted.
+ */
+ void assertClause(CVC4::prop::minisat::vec<CVC4::prop::minisat::Lit> & c);
+
+
+ /** The CNF converter in use */
+ //CVC4::prop::CnfConverter d_cnfConverter;
+ CVC4::prop::CnfStream *d_cnfStream;
public:
/**
* Create a PropEngine with a particular decision and theory engine.
*/
CVC4_PUBLIC PropEngine(CVC4::DecisionEngine&, CVC4::TheoryEngine&);
+ CVC4_PUBLIC ~PropEngine();
+
+ /**
+ * Converts the given formula to CNF and assert the CNF to the sat solver.
+ */
+ void assertFormula(const Node& node);
/**
- * Converts to CNF if necessary.
+ * Currently this takes a well-formed* Node,
+ * converts it to a propositionally equisatisifiable formula for a sat solver,
+ * and invokes the sat solver for a satisfying assignment.
+ * TODO: what does well-formed mean here?
*/
- void solve(Node);
+ void solve();
};/* class PropEngine */
+
+inline bool PropEngine::isNodeMapped(const Node & n) const{
+ return d_atom2lit.find(n) != d_atom2lit.end();
+}
+
+inline CVC4::prop::minisat::Lit PropEngine::lookupLit(const Node & n) const{
+ Assert(isNodeMapped(n));
+ return d_atom2lit.find(n)->second;
+}
+
+
+
}/* CVC4 namespace */
#endif /* __CVC4__PROP_ENGINE_H */
libsmt_la_SOURCES = \
smt_engine.cpp \
- smt_engine.h \
- cnf_converter.h \
- cnf_converter.cpp \
- cnf_conversion.h
+ smt_engine.h
+++ /dev/null
-/********************* -*- C++ -*- */
-/** cnf_conversion.h
- ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** A type for describing possible CNF conversions.
- **/
-
-#ifndef __CVC4__CNF_CONVERSION_H
-#define __CVC4__CNF_CONVERSION_H
-
-namespace CVC4 {
-
-enum CnfConversion {
- CNF_DIRECT_EXPONENTIAL = 0,
- CNF_VAR_INTRODUCTION = 1
-};
-
-inline std::ostream& operator<<(std::ostream&, CVC4::CnfConversion) CVC4_PUBLIC;
-inline std::ostream& operator<<(std::ostream& out, CVC4::CnfConversion c) {
- using namespace CVC4;
-
- switch(c) {
- case CNF_DIRECT_EXPONENTIAL:
- out << "CNF_DIRECT_EXPONENTIAL";
- break;
- case CNF_VAR_INTRODUCTION:
- out << "CNF_VAR_INTRODUCTION";
- break;
- default:
- out << "UNKNOWN-CONVERTER!" << int(c);
- }
-
- return out;
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CNF_CONVERSION_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** cnf_converter.cpp
- ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** A CNF converter for CVC4.
- **/
-
-#include "smt/cnf_converter.h"
-#include "expr/node_builder.h"
-#include "expr/node.h"
-#include "util/output.h"
-#include "util/Assert.h"
-
-namespace CVC4 {
-namespace smt {
-
-static void printAST(std::ostream& out, const Node& n, int indent = 0) {
- for(int i = 0; i < indent; ++i) {
- out << " ";
- }
- if(n.getKind() == VARIABLE) {
- out << "(VARIABLE " << n.getId();
- } else {
- out << "(" << n.getKind();
- if(n.getNumChildren() > 0) {
- out << std::endl;
- }
- for(Node::iterator i = n.begin(); i != n.end(); ++i) {
- printAST(out, *i, indent + 1);
- }
- if(n.getNumChildren() > 0) {
- for(int i = 0; i < indent; ++i) {
- out << " ";
- }
- }
- }
- out << ")" << std::endl;
-}
-
-Node CnfConverter::convert(const Node& e) {
- if(d_conversion == CNF_DIRECT_EXPONENTIAL) {
- return doConvert(e, NULL);
- }
-
- NodeBuilder<> b(AND);
- Node f = doConvert(e, &b);
-
- Debug("cnf") << "side conditions are:\n";
- NodeBuilder<> c = b;
- printAST(Debug("cnf"), c);
-
- if(f.getKind() == AND) {
- for(Node::iterator i = f.begin(); i != f.end(); ++i) {
- Debug("cnf") << "adding condition:\n";
- printAST(Debug("cnf"), *i);
- b << *i;
- }
- } else {
- Debug("cnf") << "adding condition:\n";
- printAST(Debug("cnf"), f);
- b << f;
- }
- return b;
-}
-
-Node CnfConverter::doConvert(const Node& e, NodeBuilder<>* sideConditions) {
- Node n;
-
- if(conversionMapped(e)) {
- Debug("cnf") << "conversion for " << e << " with id " << e.getId() << " is cached!" << std::endl;
- n = getConversionMap(e);
- } else {
- switch(d_conversion) {
-
- case CNF_DIRECT_EXPONENTIAL:
- Debug("cnf") << "direct conversion for " << e << " with id " << e.getId() << " is being computed!" << std::endl;
- n = directConvert(e, sideConditions);
- break;
-
- case CNF_VAR_INTRODUCTION: {
- Debug("cnf") << "var-intro conversion for " << e << " with id " << e.getId() << " is being computed!" << std::endl;
- std::vector<Node> v;
- n = varIntroductionConvert(e, sideConditions);
- Debug("cnf") << "got" << std::endl;
- printAST(Debug("cnf"), n);
-
- break;
- }
-
- default:
- Unhandled(d_conversion);
- }
-
- Debug("cnf") << "mapping conversion " << e << " with id " << e.getId() << " to " << n << " with id " << n.getId() << std::endl;
- mapConversion(e, n);
- Assert(conversionMapped(e));
- Assert(getConversionMap(e) == n);
- }
-
- Debug("cnf") << "CONVERTED ================" << std::endl;
- printAST(Debug("cnf"), e);
- Debug("cnf") << "TO ================" << std::endl;
- printAST(Debug("cnf"), n);
- Debug("cnf") << "==========================" << std::endl;
-
- return n;
-}
-
-Node CnfConverter::compressNOT(const Node& e, NodeBuilder<>* sideConditions) {
- Assert(e.getKind() == NOT);
-
- Node f = doConvert(e[0], sideConditions);
-
- Debug("stari") << "compress-not " << e.getId() << "\n";
-
- // short-circuit trivial NOTs
- if(f.getKind() == TRUE) {
- return d_nm->mkNode(FALSE);
- } else if(f.getKind() == FALSE) {
- return d_nm->mkNode(TRUE);
- } else if(f.getKind() == NOT) {
- return doConvert(f[0], sideConditions);
- } else if(f.getKind() == AND) {
- Debug("stari") << "not-converting a NOT AND\nstarted with\n";
- printAST(Debug("stari"), e[0]);
- Debug("stari") << "now have\n";
- printAST(Debug("stari"), f);
- NodeBuilder<> n(OR);
- for(Node::iterator i = f.begin(); i != f.end(); ++i) {
- if((*i).getKind() == NOT) {
- n << (*i)[0];
- } else {
- n << d_nm->mkNode(NOT, *i);
- }
- }
- return n;
- } else if(f.getKind() == OR) {
- NodeBuilder<> n(AND);
- for(Node::iterator i = f.begin(); i != f.end(); ++i) {
- if((*i).getKind() == NOT) {
- n << (*i)[0];
- } else {
- n << d_nm->mkNode(NOT, *i);
- }
- }
- return n;
- } else {
- return d_nm->mkNode(NOT, f);
- }
-}
-
-
-Node CnfConverter::directConvert(const Node& e, NodeBuilder<>* sideConditions) {
- switch(e.getKind()) {
-
- case NOT:
- return compressNOT(e, sideConditions);
-
- case AND:
- return flatten<AND>(e, sideConditions);
-
- case OR: {
- Node n = flatten<OR>(e, sideConditions);
-
- NodeBuilder<> m(OR);
- Debug("dor") << "calling directOrHelper on\n";
- printAST(Debug("dor"), n);
- directOrHelper(n.begin(), n.end(), m, sideConditions);
-
- return m;
- }
-
- case IMPLIES: {
- Assert( e.getNumChildren() == 2 );
- // just turn x IMPLIES y into (NOT x) OR y
- Node x = doConvert(e[0], sideConditions);
- Node y = doConvert(e[1], sideConditions);
- return doConvert(d_nm->mkNode(OR, doConvert(d_nm->mkNode(NOT, x), sideConditions), y), sideConditions);
- }
-
- case IFF:
- if(e.getNumChildren() == 2) {
- // common case:
- // just turn x IFF y into (x AND y) OR ((NOT x) AND (NOT y))
- Node x = doConvert(e[0], sideConditions);
- Node y = doConvert(e[1], sideConditions);
- Node r = d_nm->mkNode(OR,
- doConvert(d_nm->mkNode(AND, x, y), sideConditions),
- doConvert(d_nm->mkNode(AND,
- doConvert(d_nm->mkNode(NOT, x), sideConditions),
- doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions));
- Debug("cnf") << "working on an IFF\n";
- printAST(Debug("cnf"), e);
- Debug("cnf") << "which is\n";
- printAST(Debug("cnf"), r);
- return doConvert(r, sideConditions);
- } else {
- // more than 2 children:
- // treat x IFF y IFF z as (x IFF y) AND (y IFF z) ...
- Node::iterator i = e.begin();
- Node x = doConvert(*i++, sideConditions);
- NodeBuilder<> r(AND);
- while(i != e.end()) {
- Node y = doConvert(*i++, sideConditions);
- // now we just have two:
- // just turn x IFF y into (x AND y) OR ((NOT x) AND (NOT y))
- r << d_nm->mkNode(OR,
- doConvert(d_nm->mkNode(AND, x, y), sideConditions),
- doConvert(d_nm->mkNode(AND,
- doConvert(d_nm->mkNode(NOT, x), sideConditions),
- doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions));
- x = y;
- }
- return doConvert(r, sideConditions);
- }
-
- case XOR:
- Assert( e.getNumChildren() == 2 );
- // just turn x XOR y into (x AND (NOT y)) OR ((NOT x) AND y)
- return doConvert(d_nm->mkNode(OR,
- d_nm->mkNode(AND,
- e[0],
- d_nm->mkNode(NOT, e[1])),
- d_nm->mkNode(AND,
- d_nm->mkNode(NOT, e[0]),
- e[1])), sideConditions);
-
- default:
- // variable or theory atom
- return e;
- }
-}
-
-/**
- * OR: all ORs and NOTs
- * -- do nothing
- *
- * find an AND.
- * prefix: a \/ b \/ c
- * and term: d /\ e
- * rest: f \/ g \/ h
- *
- * construct: prefix \/ child
- *
- * then, process rest.
- *
- * if rest has no additional ANDs
- * then I get prefix \/ child \/ rest
- * and I do same with other children
- *
- * if rest has additional ANDs
- * then I get (prefix \/ child \/ rest'1) /\ (prefix \/ child \/ rest'2) /\ ...
- * and I do same with other children
- */
-void CnfConverter::directOrHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result, NodeBuilder<>* sideConditions) {
- static int nextID = 0;
- int ID = ++nextID;
- Debug("dor") << "beginning of directOrHelper " << ID << "\n";
-
- while(p != end) {
- // for each child of the expression:
-
- Debug("dor") << "CHILD == directOrHelper " << ID << "\n";
- printAST(Debug("dor"), *p);
-
- // convert the child first
- Node n = doConvert(*p, sideConditions);
-
- Debug("dor") << "CNV CHILD == directOrHelper " << ID << "\n";
- printAST(Debug("dor"), *p);
-
- // if the child is an AND
- if(n.getKind() == AND) {
- Debug("dor") << "directOrHelper found AND " << ID << "\n";
-
- NodeBuilder<> prefix = result;
- result.clear(AND);
-
- for(Node::iterator i = n.begin(); i != n.end(); ++i) {
- // for each child of the AND
- NodeBuilder<> r = prefix;
-
- Debug("dor") << "directOrHelper AND " << ID << ", converting\n";
- printAST(Debug("dor"), *i);
-
- r << doConvert(*i, sideConditions);
- NodeBuilder<> rx = r;
- Debug("dor") << "prefix \\/ child is " << ID << "\n";
- printAST(Debug("dor"), rx);
- Node::iterator p2 = p;
- directOrHelper(++p2, end, r, sideConditions);
-
- Debug("dor") << "directOrHelper recursion done " << ID << "\n";
- Node rr = r;
- Debug("dor") << "directOrHelper subterm of AND " << ID << "\n";
- printAST(Debug("dor"), rr);
-
- result << rr;
- }
-
- Debug("dor") << "end of directOrHelper AND " << ID << "\n";
- NodeBuilder<> resultnb = result;
- printAST(Debug("dor"), resultnb);
-
- return;
- } else {
- // if it's not an AND, pass it through, it's fine
- result << n;
- }
-
- Debug("cnf") << " ** result now " << result << std::endl;
-
- ++p;
- }
-
- Debug("dor") << "end of directOrHelper NO AND " << ID << "\n";
- NodeBuilder<> resultnb = result;
- printAST(Debug("dor"), resultnb);
-}
-
-Node CnfConverter::varIntroductionConvert(const Node& e, NodeBuilder<>* sideConditions) {
- switch(e.getKind()) {
-
- case NOT: {
- Node f = compressNOT(e, sideConditions);
- Debug("stari") << "compressNOT:\n";
- printAST(Debug("stari"), e);
- printAST(Debug("stari"), f);
- return f;
- }
-
- case AND: {
- Node n = flatten<AND>(e, sideConditions);
- Node var = d_nm->mkVar();
- Node notVar = d_nm->mkNode(NOT, var);
- for(Node::iterator i = n.begin(); i != n.end(); ++i) {
- // *i has already been converted by flatten<>()
- if((*i).getKind() == OR) {
- NodeBuilder<> b(OR);
- b << notVar;
- for(Node::iterator j = (*i).begin(); j != (*i).end(); ++j) {
- b << *j;
- }
- *sideConditions << b;
- } else {
- Debug("stari") << "*i should have been flattened:\n";
- printAST(Debug("stari"), *i);
- Node x = convert(*i);
- printAST(Debug("stari"), x);
- //Assert(x == *i);
- *sideConditions << d_nm->mkNode(OR, notVar, *i);
- }
- }
-
- return var;
- }
-
- case OR:
- return flatten<OR>(e, sideConditions);
-
- case IMPLIES: {
- Assert( e.getNumChildren() == 2 );
- // just turn x IMPLIES y into (NOT x) OR y
- Node x = doConvert(e[0], sideConditions);
- Node y = doConvert(e[1], sideConditions);
- return doConvert(d_nm->mkNode(OR, doConvert(d_nm->mkNode(NOT, x), sideConditions), y), sideConditions);
- }
-
- case IFF:
- if(e.getNumChildren() == 2) {
- // common case:
- // just turn x IFF y into (x AND y) OR ((NOT x) AND (NOT y))
- Node x = doConvert(e[0], sideConditions);
- Node y = doConvert(e[1], sideConditions);
- Node r = d_nm->mkNode(OR,
- doConvert(d_nm->mkNode(AND, x, y), sideConditions),
- doConvert(d_nm->mkNode(AND,
- doConvert(d_nm->mkNode(NOT, x), sideConditions),
- doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions));
- Debug("cnf") << "working on an IFF\n";
- printAST(Debug("cnf"), e);
- Debug("cnf") << "which is\n";
- printAST(Debug("cnf"), r);
- return doConvert(r, sideConditions);
- } else {
- // more than 2 children:
- // treat x IFF y IFF z as (x IFF y) AND (y IFF z) ...
- Node::iterator i = e.begin();
- Node x = doConvert(*i++, sideConditions);
- NodeBuilder<> r(AND);
- while(i != e.end()) {
- Node y = doConvert(*i++, sideConditions);
- // now we just have two:
- // just turn x IFF y into (x AND y) OR ((NOT x) AND (NOT y))
- r << d_nm->mkNode(OR,
- doConvert(d_nm->mkNode(AND, x, y), sideConditions),
- doConvert(d_nm->mkNode(AND,
- doConvert(d_nm->mkNode(NOT, x), sideConditions),
- doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions));
- x = y;
- }
- return doConvert(r, sideConditions);
- }
-
- case XOR:
- Assert( e.getNumChildren() == 2 );
- // just turn x XOR y into (x AND (NOT y)) OR ((NOT x) AND y)
- return doConvert(d_nm->mkNode(OR,
- d_nm->mkNode(AND,
- e[0],
- d_nm->mkNode(NOT, e[1])),
- d_nm->mkNode(AND,
- d_nm->mkNode(NOT, e[0]),
- e[1])), sideConditions);
-
- default:
- // variable or theory atom
- return e;
- }
-}
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** cnf_converter.h
- ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** A CNF converter for CVC4.
- **/
-
-#ifndef __CVC4__SMT__CNF_CONVERTER_H
-#define __CVC4__SMT__CNF_CONVERTER_H
-
-#include "expr/node_builder.h"
-#include "expr/node.h"
-#include "smt/cnf_conversion.h"
-
-#include <map>
-
-namespace CVC4 {
-namespace smt {
-
-class CnfConverter {
-
-private:
-
- /** Our node manager */
- NodeManager *d_nm;
-
- /** The type of conversion this converter performs */
- CVC4::CnfConversion d_conversion;
-
- /** Map of already-converted Nodes */
- std::map<Node, Node> d_conversionMap;
-
- /**
- * Returns true iff the CNF conversion for the Node was cached
- * previously.
- */
- bool conversionMapped(const Node& n) {
- return d_conversionMap.find(n) != d_conversionMap.end();
- }
-
- /**
- * Returns true iff the CNF conversion for the Node was cached
- * previously.
- */
- Node getConversionMap(const Node& n) {
- return d_conversionMap[n];
- }
-
- /**
- * Cache a new CNF conversion.
- */
- void mapConversion(const Node& n, const Node& m) {
- d_conversionMap[n] = m;
- }
-
- /**
- * Compress a NOT: do NNF transformation plus a bit. Does DNE,
- * NOT FALSE ==> TRUE, NOT TRUE ==> FALSE, and pushes NOT inside
- * of ANDs and ORs. Calls doConvert() on subnodes.
- */
- Node compressNOT(const Node& e, NodeBuilder<>* sideConditions);
-
- /**
- * Flatten a Node of kind K. K here is going to be AND or OR.
- * "Flattening" means to take all children of the Node with the same
- * kind and hoist their children to the top-level. So e.g.
- * (AND (AND x y) (AND (AND z)) w) ==> (AND x y z w).
- */
- template <CVC4::Kind K>
- Node flatten(const Node& e, NodeBuilder<>* sideConditions);
-
- /**
- * Do a direct CNF conversion (with possible exponential blow-up in
- * the number of clauses). No new variables are introduced. The
- * output is equivalent to the input.
- */
- Node directConvert(const Node& e, NodeBuilder<>* sideConditions);
-
- /**
- * Helper method for "direct" CNF preprocessing. CNF-converts an OR.
- */
- void directOrHelper(Node::iterator p,
- Node::iterator end,
- NodeBuilder<>& result,
- NodeBuilder<>* sideConditions);
-
- /**
- * Do a satisfiability-preserving CNF conversion with variable
- * introduction. Doesn't suffer from exponential blow-up in the
- * number of clauses, but new variables are introduced and the
- * output is equisatisfiable (but not equivalent) to the input.
- */
- Node varIntroductionConvert(const Node& e, NodeBuilder<>* sideConditions);
-
- /**
- * Convert an expression into CNF. If a conversion already exists
- * for the Node, it is returned. If a conversion doesn't exist, it
- * is computed and returned (caching the result).
- */
- Node doConvert(const Node& e, NodeBuilder<>* sideconditions);
-
-public:
-
- /**
- * Construct a CnfConverter.
- */
- CnfConverter(NodeManager* nm, CVC4::CnfConversion cnv = CNF_VAR_INTRODUCTION) :
- d_nm(nm),
- d_conversion(cnv) {}
-
- /**
- * Convert an expression into CNF. If a conversion already exists
- * for the Node, it is returned. If a conversion doesn't exist, it
- * is computed and returned (caching the result).
- */
- Node convert(const Node& e);
-
-};/* class CnfConverter */
-
-template <CVC4::Kind K>
-struct flatten_traits;
-
-template <>
-struct flatten_traits<AND> {
- static const CVC4::Kind ignore = TRUE; // TRUE AND x == x
- static const CVC4::Kind shortout = FALSE; // FALSE AND x == FALSE
-};
-
-template <>
-struct flatten_traits<OR> {
- static const CVC4::Kind ignore = FALSE; // FALSE OR x == x
- static const CVC4::Kind shortout = TRUE; // TRUE OR x == TRUE
-};
-
-template <CVC4::Kind K>
-Node CnfConverter::flatten(const Node& e, NodeBuilder<>* sideConditions) {
- Assert(e.getKind() == K);
-
- NodeBuilder<> n(K);
-
- for(Node::iterator i = e.begin(); i != e.end(); ++i) {
- Node f = doConvert(*i, sideConditions);
- if(f.getKind() == K) {
- for(Node::iterator j = f.begin(); j != f.end(); ++j) {
- n << *j;
- }
- } else if(f.getKind() == flatten_traits<K>::ignore) {
- /* do nothing */
- } else if(f.getKind() == flatten_traits<K>::shortout) {
- return f;
- } else {
- n << f;
- }
- }
-
- return n;
-}
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SMT__CNF_CONVERTER_H */
d_opts(opts),
d_de(),
d_te(),
- d_prop(d_de, d_te),
- d_cnfConverter(d_nm, opts->d_cnfConversion) {
+ d_prop(d_de, d_te){
}
SmtEngine::~SmtEngine() {
return e;
}
-Node SmtEngine::processAssertionList() {
- if(d_assertions.size() == 1) {
- return d_assertions[0];
+void SmtEngine::processAssertionList() {
+ for(unsigned i = 0; i < d_assertions.size(); ++i) {
+ d_prop.assertFormula(d_assertions[i]);
}
-
- NodeBuilder<> asserts(AND);
- for(std::vector<Node>::iterator i = d_assertions.begin();
- i != d_assertions.end();
- ++i) {
- asserts << *i;
- }
-
d_assertions.clear();
- d_assertions.push_back(asserts);
- return d_assertions[0];
}
-static void printAST(std::ostream& out, const Node& n, int indent = 0) {
- for(int i = 0; i < indent; ++i) {
- out << " ";
- }
- if(n.getKind() == VARIABLE) {
- out << "(VARIABLE " << n.getId();
- } else {
- out << "(" << n.getKind();
- if(n.getNumChildren() > 0) {
- out << std::endl;
- }
- for(Node::iterator i = n.begin(); i != n.end(); ++i) {
- printAST(out, *i, indent + 1);
- }
- if(n.getNumChildren() > 0) {
- for(int i = 0; i < indent; ++i) {
- out << " ";
- }
- }
- }
- out << ")" << std::endl;
-}
Result SmtEngine::check() {
Debug("smt") << "SMT check()" << std::endl;
- Node asserts = processAssertionList();
-
- // CNF conversion
- Debug("cnf") << "preprocessing " << asserts << std::endl;
- Node assertsOut = d_cnfConverter.convert(asserts);
- Debug("cnf") << " and got " << assertsOut << std::endl;
-
- Debug("smt") << "BEFORE CONVERSION ==" << std::endl;
- printAST(Debug("smt"), asserts);
- Debug("smt") << "AFTER CONVERSION ==" << std::endl;
- printAST(Debug("smt"), assertsOut);
- Debug("smt") << "===================" << std::endl;
-
- d_prop.solve(assertsOut);
+ processAssertionList();
+ d_prop.solve();
return Result(Result::VALIDITY_UNKNOWN);
}
#include "util/options.h"
#include "prop/prop_engine.h"
#include "util/decision_engine.h"
-#include "smt/cnf_converter.h"
// In terms of abstraction, this is below (and provides services to)
// ValidityChecker and above (and requires the services of)
/** The propositional engine */
PropEngine d_prop;
- /** The CNF converter in use */
- CVC4::smt::CnfConverter d_cnfConverter;
/**
* Pre-process an Node. This is expected to be highly-variable,
* Process the assertion list: for literals and conjunctions of
* literals, assert to T-solver.
*/
- Node processAssertionList();
+ void processAssertionList();
};/* class SmtEngine */
#include <iostream>
#include "parser/parser.h"
-#include "smt/cnf_conversion.h"
+#include "prop/cnf_conversion.h"
namespace CVC4 {
projects / cvc5.git / commitdiff