From: Tim King Date: Tue, 2 Feb 2010 20:56:47 +0000 (+0000) Subject: Switched cnf conversion to go through CnfStream. X-Git-Tag: cvc5-1.0.0~9314 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a8588cb23c5257bb11a70348346476b55317faa3;p=cvc5.git Switched cnf conversion to go through CnfStream. --- diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 3473de30f..fc0697eda 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -8,6 +8,9 @@ noinst_LTLIBRARIES = libprop.la libprop_la_SOURCES = \ prop_engine.cpp \ prop_engine.h \ - sat.h + sat.h \ + cnf_stream.h \ + cnf_stream.cpp \ + cnf_conversion.h SUBDIRS = minisat diff --git a/src/prop/cnf_conversion.h b/src/prop/cnf_conversion.h new file mode 100644 index 000000000..924cae063 --- /dev/null +++ b/src/prop/cnf_conversion.h @@ -0,0 +1,46 @@ +/********************* -*- 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 */ diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp new file mode 100644 index 000000000..73c3f6c01 --- /dev/null +++ b/src/prop/cnf_stream.cpp @@ -0,0 +1,421 @@ +/********************* -*- 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 + +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 & c){ + d_propEngine->assertClause(c); +} + +void CnfStream::insertClauseIntoStream(minisat::Lit a){ + vec clause(1); + clause[0] = a; + insertClauseIntoStream(clause); +} +void CnfStream::insertClauseIntoStream(minisat::Lit a,minisat::Lit b){ + vec clause(2); + clause[0] = a; + clause[1] = b; + insertClauseIntoStream(clause); +} +void CnfStream::insertClauseIntoStream(minisat::Lit a,minisat::Lit b, minisat::Lit c){ + vec 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 & 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 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 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 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 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 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 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 */ diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h new file mode 100644 index 000000000..c0a70730a --- /dev/null +++ b/src/prop/cnf_stream.h @@ -0,0 +1,165 @@ +/********************* -*- 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 + +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 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 & 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 & 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 */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index bc46e39d5..875d0cd16 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -13,6 +13,8 @@ **/ #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" @@ -30,123 +32,47 @@ using namespace std; 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 & 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* vars, map* 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* vars, Node e, vec* c) { - if(e.getKind() == VARIABLE) { - map::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::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* vars, map* varsReverse, Node e) { - vec 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 vars; - std::map 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 */ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 6e1f8cb61..f356c9e0b 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -25,6 +25,13 @@ #include "prop/minisat/core/SolverTypes.h" #include +#include "prop/cnf_stream.h" + +namespace CVC4 { + namespace prop { + class CnfStream; + } +} namespace CVC4 { @@ -35,25 +42,80 @@ namespace CVC4 { class PropEngine { DecisionEngine &d_de; TheoryEngine &d_te; - //CVC4::prop::minisat::SimpSolver d_sat; - //std::map d_vars; - //std::map d_varsReverse; - void addVars(CVC4::prop::minisat::SimpSolver*, std::map*, std::map*, 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 d_atom2lit; + std::map 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 & 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 */ diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index fa7fed5f1..a2da2c949 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -7,7 +7,4 @@ noinst_LTLIBRARIES = libsmt.la libsmt_la_SOURCES = \ smt_engine.cpp \ - smt_engine.h \ - cnf_converter.h \ - cnf_converter.cpp \ - cnf_conversion.h + smt_engine.h diff --git a/src/smt/cnf_conversion.h b/src/smt/cnf_conversion.h deleted file mode 100644 index 924cae063..000000000 --- a/src/smt/cnf_conversion.h +++ /dev/null @@ -1,46 +0,0 @@ -/********************* -*- 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 */ diff --git a/src/smt/cnf_converter.cpp b/src/smt/cnf_converter.cpp deleted file mode 100644 index 7c53e9b04..000000000 --- a/src/smt/cnf_converter.cpp +++ /dev/null @@ -1,431 +0,0 @@ -/********************* -*- 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 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(e, sideConditions); - - case OR: { - Node n = flatten(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(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(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 */ diff --git a/src/smt/cnf_converter.h b/src/smt/cnf_converter.h deleted file mode 100644 index 7b7be0480..000000000 --- a/src/smt/cnf_converter.h +++ /dev/null @@ -1,170 +0,0 @@ -/********************* -*- 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 - -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 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 - 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 -struct flatten_traits; - -template <> -struct flatten_traits { - static const CVC4::Kind ignore = TRUE; // TRUE AND x == x - static const CVC4::Kind shortout = FALSE; // FALSE AND x == FALSE -}; - -template <> -struct flatten_traits { - static const CVC4::Kind ignore = FALSE; // FALSE OR x == x - static const CVC4::Kind shortout = TRUE; // TRUE OR x == TRUE -}; - -template -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::ignore) { - /* do nothing */ - } else if(f.getKind() == flatten_traits::shortout) { - return f; - } else { - n << f; - } - } - - return n; -} - -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__SMT__CNF_CONVERTER_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c0f825462..7e2b6e24c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -27,8 +27,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() : 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() { @@ -43,62 +42,18 @@ Node SmtEngine::preprocess(const Node& e) { 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::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); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index b073a68c9..097500833 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -29,7 +29,6 @@ #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) @@ -134,8 +133,6 @@ private: /** 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, @@ -167,7 +164,7 @@ private: * Process the assertion list: for literals and conjunctions of * literals, assert to T-solver. */ - Node processAssertionList(); + void processAssertionList(); };/* class SmtEngine */ diff --git a/src/util/options.h b/src/util/options.h index 2e696d0db..ff156b595 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -18,7 +18,7 @@ #include #include "parser/parser.h" -#include "smt/cnf_conversion.h" +#include "prop/cnf_conversion.h" namespace CVC4 {