diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
commit | 25e9c72dd689d3b621b901220794c652a3ba589a (patch) | |
tree | 58b14dd3818f3e7a8ca3311a0457716e7753a95e /src | |
parent | 587520ce888b88294fb9e4ca476e2425d8bf026e (diff) |
merge from symmetry branch
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/command.cpp | 135 | ||||
-rw-r--r-- | src/expr/command.h | 43 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 171 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.h | 1 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 169 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 1 | ||||
-rw-r--r-- | src/printer/printer.h | 5 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.cpp | 13 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.h | 1 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 180 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 1 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 14 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 22 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 12 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 8 | ||||
-rw-r--r-- | src/theory/uf/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.cpp | 14 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.h | 3 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 616 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 160 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 20 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 9 | ||||
-rw-r--r-- | src/util/options.cpp | 19 | ||||
-rw-r--r-- | src/util/options.h | 9 |
24 files changed, 1472 insertions, 158 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 8d6748e54..2783e8eaa 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -27,21 +27,26 @@ #include "smt/bad_option_exception.h" #include "util/output.h" #include "util/sexpr.h" +#include "expr/node.h" +#include "printer/printer.h" using namespace std; namespace CVC4 { std::ostream& operator<<(std::ostream& out, const Command& c) { - c.toStream(out); + c.toStream(out, + Node::setdepth::getDepth(out), + Node::printtypes::getPrintTypes(out), + Node::setlanguage::getLanguage(out)); return out; } -ostream& operator<<(ostream& out, const Command* command) { - if(command == NULL) { +ostream& operator<<(ostream& out, const Command* c) { + if(c == NULL) { out << "null"; } else { - command->toStream(out); + out << *c; } return out; } @@ -59,6 +64,11 @@ std::string Command::toString() const { return ss.str(); } +void Command::toStream(std::ostream& out, int toDepth, bool types, + OutputLanguage language) const { + Printer::getPrinter(language)->toStream(out, this, toDepth, types); +} + void Command::printResult(std::ostream& out) const { } @@ -72,10 +82,6 @@ void EmptyCommand::invoke(SmtEngine* smtEngine) { /* empty commands have no implementation */ } -void EmptyCommand::toStream(std::ostream& out) const { - out << "EmptyCommand(" << d_name << ")"; -} - /* class AssertCommand */ AssertCommand::AssertCommand(const BoolExpr& e) : @@ -86,30 +92,18 @@ void AssertCommand::invoke(SmtEngine* smtEngine) { smtEngine->assertFormula(d_expr); } -void AssertCommand::toStream(std::ostream& out) const { - out << "Assert(" << d_expr << ")"; -} - /* class PushCommand */ void PushCommand::invoke(SmtEngine* smtEngine) { smtEngine->push(); } -void PushCommand::toStream(std::ostream& out) const { - out << "Push()"; -} - /* class PopCommand */ void PopCommand::invoke(SmtEngine* smtEngine) { smtEngine->pop(); } -void PopCommand::toStream(std::ostream& out) const { - out << "Pop()"; -} - /* class CheckSatCommand */ CheckSatCommand::CheckSatCommand(const BoolExpr& expr) : @@ -120,14 +114,6 @@ void CheckSatCommand::invoke(SmtEngine* smtEngine) { d_result = smtEngine->checkSat(d_expr); } -void CheckSatCommand::toStream(std::ostream& out) const { - if(d_expr.isNull()) { - out << "CheckSat()"; - } else { - out << "CheckSat(" << d_expr << ")"; - } -} - Result CheckSatCommand::getResult() const { return d_result; } @@ -154,19 +140,11 @@ void QueryCommand::printResult(std::ostream& out) const { out << d_result << endl; } -void QueryCommand::toStream(std::ostream& out) const { - out << "Query(" << d_expr << ')'; -} - /* class QuitCommand */ QuitCommand::QuitCommand() { } -void QuitCommand::toStream(std::ostream& out) const { - out << "Quit()" << endl; -} - /* class CommandSequence */ CommandSequence::CommandSequence() : @@ -197,14 +175,6 @@ void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) { } } -void CommandSequence::toStream(std::ostream& out) const { - out << "CommandSequence[" << endl; - for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { - out << *d_commandSequence[i] << endl; - } - out << "]"; -} - /* class DeclarationCommand */ DeclarationCommand::DeclarationCommand(const std::string& id, Type t) : @@ -225,14 +195,6 @@ Type DeclarationCommand::getDeclaredType() const { return d_type; } -void DeclarationCommand::toStream(std::ostream& out) const { - out << "Declare(["; - copy( d_declaredSymbols.begin(), d_declaredSymbols.end() - 1, - ostream_iterator<string>(out, ", ") ); - out << d_declaredSymbols.back(); - out << "])"; -} - /* class DefineFunctionCommand */ DefineFunctionCommand::DefineFunctionCommand(Expr func, @@ -247,16 +209,6 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { smtEngine->defineFunction(d_func, d_formals, d_formula); } -void DefineFunctionCommand::toStream(std::ostream& out) const { - out << "DefineFunction( \"" << d_func << "\", ["; - if(d_formals.size() > 0) { - copy( d_formals.begin(), d_formals.end() - 1, - ostream_iterator<Expr>(out, ", ") ); - out << d_formals.back(); - } - out << "], << " << d_formula << " >> )"; -} - /* class DefineFunctionCommand */ DefineNamedFunctionCommand::DefineNamedFunctionCommand(Expr func, @@ -273,12 +225,6 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) { } } -void DefineNamedFunctionCommand::toStream(std::ostream& out) const { - out << "DefineNamedFunction( "; - this->DefineFunctionCommand::toStream(out); - out << " )"; -} - /* class Simplify */ SimplifyCommand::SimplifyCommand(Expr term) : @@ -286,7 +232,7 @@ SimplifyCommand::SimplifyCommand(Expr term) : } void SimplifyCommand::invoke(SmtEngine* smtEngine) { -#warning TODO: what is this + d_result = smtEngine->simplify(d_term); } Expr SimplifyCommand::getResult() const { @@ -297,10 +243,6 @@ void SimplifyCommand::printResult(std::ostream& out) const { out << d_result << endl; } -void SimplifyCommand::toStream(std::ostream& out) const { - out << "Simplify( << " << d_term << " >> )"; -} - /* class GetValueCommand */ GetValueCommand::GetValueCommand(Expr term) : @@ -320,10 +262,6 @@ void GetValueCommand::printResult(std::ostream& out) const { out << d_result << endl; } -void GetValueCommand::toStream(std::ostream& out) const { - out << "GetValue( << " << d_term << " >> )"; -} - /* class GetAssignmentCommand */ GetAssignmentCommand::GetAssignmentCommand() { @@ -341,10 +279,6 @@ void GetAssignmentCommand::printResult(std::ostream& out) const { out << d_result << endl; } -void GetAssignmentCommand::toStream(std::ostream& out) const { - out << "GetAssignment()"; -} - /* class GetAssertionsCommand */ GetAssertionsCommand::GetAssertionsCommand() { @@ -365,10 +299,6 @@ void GetAssertionsCommand::printResult(std::ostream& out) const { out << d_result; } -void GetAssertionsCommand::toStream(std::ostream& out) const { - out << "GetAssertions()"; -} - /* class SetBenchmarkStatusCommand */ SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) : @@ -390,10 +320,6 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) { } } -void SetBenchmarkStatusCommand::toStream(std::ostream& out) const { - out << "SetBenchmarkStatus(" << d_status << ")"; -} - /* class SetBenchmarkLogicCommand */ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) : @@ -409,10 +335,6 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) { } } -void SetBenchmarkLogicCommand::toStream(std::ostream& out) const { - out << "SetBenchmarkLogic(" << d_logic << ")"; -} - /* class SetInfoCommand */ SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) : @@ -441,10 +363,6 @@ void SetInfoCommand::printResult(std::ostream& out) const { } } -void SetInfoCommand::toStream(std::ostream& out) const { - out << "SetInfo(" << d_flag << ", " << d_sexpr << ")"; -} - /* class GetInfoCommand */ GetInfoCommand::GetInfoCommand(std::string flag) : @@ -471,10 +389,6 @@ void GetInfoCommand::printResult(std::ostream& out) const { } } -void GetInfoCommand::toStream(std::ostream& out) const { - out << "GetInfo(" << d_flag << ")"; -} - /* class SetOptionCommand */ SetOptionCommand::SetOptionCommand(std::string flag, SExpr& sexpr) : @@ -503,10 +417,6 @@ void SetOptionCommand::printResult(std::ostream& out) const { } } -void SetOptionCommand::toStream(std::ostream& out) const { - out << "SetOption(" << d_flag << ", " << d_sexpr << ")"; -} - /* class GetOptionCommand */ GetOptionCommand::GetOptionCommand(std::string flag) : @@ -531,10 +441,6 @@ void GetOptionCommand::printResult(std::ostream& out) const { } } -void GetOptionCommand::toStream(std::ostream& out) const { - out << "GetOption(" << d_flag << ")"; -} - /* class DatatypeDeclarationCommand */ DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) : @@ -553,17 +459,6 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) { //smtEngine->addDatatypeDefinitions(d_datatype); } -void DatatypeDeclarationCommand::toStream(std::ostream& out) const { - out << "DatatypeDeclarationCommand(["; - for(vector<DatatypeType>::const_iterator i = d_datatypes.begin(), - i_end = d_datatypes.end(); - i != i_end; - ++i) { - out << *i << ";" << endl; - } - out << "])"; -} - /* output stream insertion operator for benchmark statuses */ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) { diff --git a/src/expr/command.h b/src/expr/command.h index d0b72c3dd..50d382038 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -62,7 +62,8 @@ public: virtual void invoke(SmtEngine* smtEngine) = 0; virtual void invoke(SmtEngine* smtEngine, std::ostream& out); virtual ~Command() {}; - virtual void toStream(std::ostream&) const = 0; + virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, + OutputLanguage language = language::output::LANG_AST) const; std::string toString() const; virtual void printResult(std::ostream& out) const; };/* class Command */ @@ -77,7 +78,7 @@ protected: public: EmptyCommand(std::string name = ""); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + std::string getName() const { return d_name; } };/* class EmptyCommand */ class CVC4_PUBLIC AssertCommand : public Command { @@ -86,19 +87,17 @@ protected: public: AssertCommand(const BoolExpr& e); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + BoolExpr getExpr() const { return d_expr; } };/* class AssertCommand */ class CVC4_PUBLIC PushCommand : public Command { public: void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; };/* class PushCommand */ class CVC4_PUBLIC PopCommand : public Command { public: void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; };/* class PopCommand */ class CVC4_PUBLIC DeclarationCommand : public EmptyCommand { @@ -110,7 +109,6 @@ public: DeclarationCommand(const std::vector<std::string>& ids, Type t); const std::vector<std::string>& getDeclaredSymbols() const; Type getDeclaredType() const; - void toStream(std::ostream& out) const; };/* class DeclarationCommand */ class CVC4_PUBLIC DefineFunctionCommand : public Command { @@ -123,7 +121,9 @@ public: const std::vector<Expr>& formals, Expr formula); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + Expr getFunction() const { return d_func; } + const std::vector<Expr>& getFormals() const { return d_formals; } + Expr getFormula() const { return d_formula; } };/* class DefineFunctionCommand */ /** @@ -137,7 +137,6 @@ public: const std::vector<Expr>& formals, Expr formula); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; };/* class DefineNamedFunctionCommand */ class CVC4_PUBLIC CheckSatCommand : public Command { @@ -147,9 +146,9 @@ protected: public: CheckSatCommand(const BoolExpr& expr); void invoke(SmtEngine* smtEngine); + BoolExpr getExpr() const { return d_expr; } Result getResult() const; void printResult(std::ostream& out) const; - void toStream(std::ostream& out) const; };/* class CheckSatCommand */ class CVC4_PUBLIC QueryCommand : public Command { @@ -159,9 +158,9 @@ protected: public: QueryCommand(const BoolExpr& e); void invoke(SmtEngine* smtEngine); + BoolExpr getExpr() const { return d_expr; } Result getResult() const; void printResult(std::ostream& out) const; - void toStream(std::ostream& out) const; };/* class QueryCommand */ // this is TRANSFORM in the CVC presentation language @@ -172,9 +171,9 @@ protected: public: SimplifyCommand(Expr term); void invoke(SmtEngine* smtEngine); + Expr getTerm() const { return d_term; } Expr getResult() const; void printResult(std::ostream& out) const; - void toStream(std::ostream& out) const; };/* class SimplifyCommand */ class CVC4_PUBLIC GetValueCommand : public Command { @@ -184,9 +183,9 @@ protected: public: GetValueCommand(Expr term); void invoke(SmtEngine* smtEngine); + Expr getTerm() const { return d_term; } Expr getResult() const; void printResult(std::ostream& out) const; - void toStream(std::ostream& out) const; };/* class GetValueCommand */ class CVC4_PUBLIC GetAssignmentCommand : public Command { @@ -197,7 +196,6 @@ public: void invoke(SmtEngine* smtEngine); SExpr getResult() const; void printResult(std::ostream& out) const; - void toStream(std::ostream& out) const; };/* class GetAssignmentCommand */ class CVC4_PUBLIC GetAssertionsCommand : public Command { @@ -208,7 +206,6 @@ public: void invoke(SmtEngine* smtEngine); std::string getResult() const; void printResult(std::ostream& out) const; - void toStream(std::ostream& out) const; };/* class GetAssertionsCommand */ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { @@ -218,7 +215,7 @@ protected: public: SetBenchmarkStatusCommand(BenchmarkStatus status); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + BenchmarkStatus getStatus() const { return d_status; } };/* class SetBenchmarkStatusCommand */ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { @@ -228,7 +225,7 @@ protected: public: SetBenchmarkLogicCommand(std::string logic); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + std::string getLogic() const { return d_logic; } };/* class SetBenchmarkLogicCommand */ class CVC4_PUBLIC SetInfoCommand : public Command { @@ -239,7 +236,8 @@ protected: public: SetInfoCommand(std::string flag, SExpr& sexpr); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + std::string getFlag() const { return d_flag; } + SExpr getSExpr() const { return d_sexpr; } std::string getResult() const; void printResult(std::ostream& out) const; };/* class SetInfoCommand */ @@ -251,7 +249,7 @@ protected: public: GetInfoCommand(std::string flag); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + std::string getFlag() const { return d_flag; } std::string getResult() const; void printResult(std::ostream& out) const; };/* class GetInfoCommand */ @@ -264,7 +262,8 @@ protected: public: SetOptionCommand(std::string flag, SExpr& sexpr); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + std::string getFlag() const { return d_flag; } + SExpr getSExpr() const { return d_sexpr; } std::string getResult() const; void printResult(std::ostream& out) const; };/* class SetOptionCommand */ @@ -276,7 +275,7 @@ protected: public: GetOptionCommand(std::string flag); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + std::string getFlag() const { return d_flag; } std::string getResult() const; void printResult(std::ostream& out) const; };/* class GetOptionCommand */ @@ -288,13 +287,12 @@ public: DatatypeDeclarationCommand(const DatatypeType& datatype); DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes); void invoke(SmtEngine* smtEngine); - void toStream(std::ostream& out) const; + const std::vector<DatatypeType>& getDatatypes() const { return d_datatypes; } };/* class DatatypeDeclarationCommand */ class CVC4_PUBLIC QuitCommand : public EmptyCommand { public: QuitCommand(); - void toStream(std::ostream& out) const; };/* class QuitCommand */ class CVC4_PUBLIC CommandSequence : public Command { @@ -309,7 +307,6 @@ public: void invoke(SmtEngine* smtEngine); void invoke(SmtEngine* smtEngine, std::ostream& out); void addCommand(Command* cmd); - void toStream(std::ostream& out) const; typedef std::vector<Command*>::iterator iterator; typedef std::vector<Command*>::const_iterator const_iterator; diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 6cdf878a0..5863ded9f 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -17,10 +17,15 @@ **/ #include "printer/ast/ast_printer.h" +#include "expr/expr.h" // for ExprSetDepth etc.. #include "util/language.h" // for LANG_AST #include "expr/node_manager.h" // for VarNameAttr +#include "expr/command.h" #include <iostream> +#include <vector> +#include <string> +#include <typeinfo> using namespace std; @@ -29,7 +34,7 @@ namespace printer { namespace ast { void AstPrinter::toStream(std::ostream& out, TNode n, - int toDepth, bool types) const { + int toDepth, bool types) const { // null if(n.getKind() == kind::NULL_EXPR) { out << "null"; @@ -92,6 +97,170 @@ void AstPrinter::toStream(std::ostream& out, TNode n, out << ')'; }/* AstPrinter::toStream() */ +template <class T> +static bool tryToStream(std::ostream& out, const Command* c); + +void AstPrinter::toStream(std::ostream& out, const Command* c, + int toDepth, bool types) const { + expr::ExprSetDepth::Scope sdScope(out, toDepth); + expr::ExprPrintTypes::Scope ptScope(out, types); + + if(tryToStream<EmptyCommand>(out, c) || + tryToStream<AssertCommand>(out, c) || + tryToStream<PushCommand>(out, c) || + tryToStream<PopCommand>(out, c) || + tryToStream<CheckSatCommand>(out, c) || + tryToStream<QueryCommand>(out, c) || + tryToStream<QuitCommand>(out, c) || + tryToStream<CommandSequence>(out, c) || + tryToStream<DeclarationCommand>(out, c) || + tryToStream<DefineFunctionCommand>(out, c) || + tryToStream<DefineNamedFunctionCommand>(out, c) || + tryToStream<SimplifyCommand>(out, c) || + tryToStream<GetValueCommand>(out, c) || + tryToStream<GetAssignmentCommand>(out, c) || + tryToStream<GetAssertionsCommand>(out, c) || + tryToStream<SetBenchmarkStatusCommand>(out, c) || + tryToStream<SetBenchmarkLogicCommand>(out, c) || + tryToStream<SetInfoCommand>(out, c) || + tryToStream<GetInfoCommand>(out, c) || + tryToStream<SetOptionCommand>(out, c) || + tryToStream<GetOptionCommand>(out, c) || + tryToStream<DatatypeDeclarationCommand>(out, c)) { + return; + } + + Unhandled("don't know how to print a Command of class: %s", typeid(*c).name()); + +}/* AstPrinter::toStream() */ + +static void toStream(std::ostream& out, const EmptyCommand* c) { + out << "EmptyCommand(" << c->getName() << ")"; +} + +static void toStream(std::ostream& out, const AssertCommand* c) { + out << "Assert(" << c->getExpr() << ")"; +} + +static void toStream(std::ostream& out, const PushCommand* c) { + out << "Push()"; +} + +static void toStream(std::ostream& out, const PopCommand* c) { + out << "Pop()"; +} + +static void toStream(std::ostream& out, const CheckSatCommand* c) { + BoolExpr e = c->getExpr(); + if(e.isNull()) { + out << "CheckSat()"; + } else { + out << "CheckSat(" << e << ")"; + } +} + +static void toStream(std::ostream& out, const QueryCommand* c) { + out << "Query(" << c->getExpr() << ')'; +} + +static void toStream(std::ostream& out, const QuitCommand* c) { + out << "Quit()"; +} + +static void toStream(std::ostream& out, const CommandSequence* c) { + out << "CommandSequence[" << endl; + for(CommandSequence::const_iterator i = c->begin(); + i != c->end(); + ++i) { + out << *i << endl; + } + out << "]"; +} + +static void toStream(std::ostream& out, const DeclarationCommand* c) { + const vector<string>& declaredSymbols = c->getDeclaredSymbols(); + out << "Declare(["; + copy( declaredSymbols.begin(), declaredSymbols.end() - 1, + ostream_iterator<string>(out, ", ") ); + out << declaredSymbols.back(); + out << "])"; +} + +static void toStream(std::ostream& out, const DefineFunctionCommand* c) { + Expr func = c->getFunction(); + const std::vector<Expr>& formals = c->getFormals(); + Expr formula = c->getFormula(); + out << "DefineFunction( \"" << func << "\", ["; + if(formals.size() > 0) { + copy( formals.begin(), formals.end() - 1, + ostream_iterator<Expr>(out, ", ") ); + out << formals.back(); + } + out << "], << " << formula << " >> )"; +} + +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { + out << "DefineNamedFunction( "; + toStream(out, static_cast<const DefineFunctionCommand*>(c)); + out << " )"; +} + +static void toStream(std::ostream& out, const SimplifyCommand* c) { + out << "Simplify( << " << c->getTerm() << " >> )"; +} + +static void toStream(std::ostream& out, const GetValueCommand* c) { + out << "GetValue( << " << c->getTerm() << " >> )"; +} + +static void toStream(std::ostream& out, const GetAssignmentCommand* c) { + out << "GetAssignment()"; +} +static void toStream(std::ostream& out, const GetAssertionsCommand* c) { + out << "GetAssertions()"; +} +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) { + out << "SetBenchmarkStatus(" << c->getStatus() << ")"; +} +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) { + out << "SetBenchmarkLogic(" << c->getLogic() << ")"; +} +static void toStream(std::ostream& out, const SetInfoCommand* c) { + out << "SetInfo(" << c->getFlag() << ", " << c->getSExpr() << ")"; +} + +static void toStream(std::ostream& out, const GetInfoCommand* c) { + out << "GetInfo(" << c->getFlag() << ")"; +} +static void toStream(std::ostream& out, const SetOptionCommand* c) { + out << "SetOption(" << c->getFlag() << ", " << c->getSExpr() << ")"; +} + +static void toStream(std::ostream& out, const GetOptionCommand* c) { + out << "GetOption(" << c->getFlag() << ")"; +} + +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { + const vector<DatatypeType>& datatypes = c->getDatatypes(); + out << "DatatypeDeclarationCommand(["; + for(vector<DatatypeType>::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); + i != i_end; + ++i) { + out << *i << ";" << endl; + } + out << "])"; +} + +template <class T> +static bool tryToStream(std::ostream& out, const Command* c) { + if(typeid(*c) == typeid(T)) { + toStream(out, dynamic_cast<const T*>(c)); + return true; + } + return false; +} + }/* CVC4::printer::ast namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index f3d927cfb..ddc3c50b8 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -32,6 +32,7 @@ namespace ast { class AstPrinter : public CVC4::Printer { public: void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; };/* class AstPrinter */ }/* CVC4::printer::ast namespace */ diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index b2b801ded..11d633271 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -17,9 +17,15 @@ **/ #include "printer/cvc/cvc_printer.h" -#include "util/language.h" +#include "expr/expr.h" // for ExprSetDepth etc.. +#include "util/language.h" // for LANG_AST +#include "expr/node_manager.h" // for VarNameAttr +#include "expr/command.h" #include <iostream> +#include <vector> +#include <string> +#include <typeinfo> #include <algorithm> #include <iterator> @@ -324,7 +330,166 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, }/* CvcPrinter::toStream() */ +template <class T> +static bool tryToStream(std::ostream& out, const Command* c); + +void CvcPrinter::toStream(std::ostream& out, const Command* c, + int toDepth, bool types) const { + expr::ExprSetDepth::Scope sdScope(out, toDepth); + expr::ExprPrintTypes::Scope ptScope(out, types); + + if(tryToStream<AssertCommand>(out, c) || + tryToStream<PushCommand>(out, c) || + tryToStream<PopCommand>(out, c) || + tryToStream<CheckSatCommand>(out, c) || + tryToStream<QueryCommand>(out, c) || + tryToStream<QuitCommand>(out, c) || + tryToStream<CommandSequence>(out, c) || + tryToStream<DeclarationCommand>(out, c) || + tryToStream<DefineFunctionCommand>(out, c) || + tryToStream<DefineNamedFunctionCommand>(out, c) || + tryToStream<SimplifyCommand>(out, c) || + tryToStream<GetValueCommand>(out, c) || + tryToStream<GetAssignmentCommand>(out, c) || + tryToStream<GetAssertionsCommand>(out, c) || + tryToStream<SetBenchmarkStatusCommand>(out, c) || + tryToStream<SetBenchmarkLogicCommand>(out, c) || + tryToStream<SetInfoCommand>(out, c) || + tryToStream<GetInfoCommand>(out, c) || + tryToStream<SetOptionCommand>(out, c) || + tryToStream<GetOptionCommand>(out, c) || + tryToStream<DatatypeDeclarationCommand>(out, c)) { + return; + } + + Unhandled("don't know how to print this command in CVC's presentation language: %s", c->toString().c_str()); + +}/* CvcPrinter::toStream() */ + +static void toStream(std::ostream& out, const AssertCommand* c) { + out << "ASSERT " << c->getExpr() << ";"; +} + +static void toStream(std::ostream& out, const PushCommand* c) { + out << "PUSH;"; +} + +static void toStream(std::ostream& out, const PopCommand* c) { + out << "POP;"; +} + +static void toStream(std::ostream& out, const CheckSatCommand* c) { + BoolExpr e = c->getExpr(); + if(!e.isNull()) { + out << "CHECKSAT " << e << ";"; + } + out << "CHECKSAT;"; +} + +static void toStream(std::ostream& out, const QueryCommand* c) { + out << "QUERY " << c->getExpr() << ";"; +} + +static void toStream(std::ostream& out, const QuitCommand* c) { + Unhandled("quit command"); +} + +static void toStream(std::ostream& out, const CommandSequence* c) { + for(CommandSequence::const_iterator i = c->begin(); + i != c->end(); + ++i) { + out << *i << endl; + } +} + +static void toStream(std::ostream& out, const DeclarationCommand* c) { + const vector<string>& declaredSymbols = c->getDeclaredSymbols(); + Type declaredType = c->getDeclaredType(); + Assert(declaredSymbols.size() > 0); + copy( declaredSymbols.begin(), declaredSymbols.end() - 1, + ostream_iterator<string>(out, ", ") ); + out << declaredSymbols.back(); + out << " : " << declaredType << ";"; +} + +static void toStream(std::ostream& out, const DefineFunctionCommand* c) { + Expr func = c->getFunction(); + const vector<Expr>& formals = c->getFormals(); + Expr formula = c->getFormula(); + out << func << " : " << func.getType() << " = LAMBDA("; + vector<Expr>::const_iterator i = formals.begin(); + while(i != formals.end()) { + out << (*i) << ":" << (*i).getType(); + if(++i != formals.end()) { + out << ", "; + } + } + out << "): " << formula << ";"; +} + +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { + toStream(out, static_cast<const DefineFunctionCommand*>(c)); +} + +static void toStream(std::ostream& out, const SimplifyCommand* c) { + out << "TRANSFORM " << c->getTerm() << ";"; +} + +static void toStream(std::ostream& out, const GetValueCommand* c) { + out << "% (get-value " << c->getTerm() << ")"; +} + +static void toStream(std::ostream& out, const GetAssignmentCommand* c) { + out << "% (get-assignment)"; +} + +static void toStream(std::ostream& out, const GetAssertionsCommand* c) { + out << "% (get-assertions)"; +} + +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) { + out << "% (set-info :status " << c->getStatus() << ")"; +} + +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) { + out << "% (set-logic " << c->getLogic() << ")"; +} + +static void toStream(std::ostream& out, const SetInfoCommand* c) { + out << "% (set-info " << c->getFlag() << " " << c->getSExpr() << ")"; +} + +static void toStream(std::ostream& out, const GetInfoCommand* c) { + out << "% (get-info " << c->getFlag() << ")"; +} + +static void toStream(std::ostream& out, const SetOptionCommand* c) { + out << "% (set-option " << c->getFlag() << " " << c->getSExpr() << ")"; +} + +static void toStream(std::ostream& out, const GetOptionCommand* c) { + out << "% (get-option " << c->getFlag() << ")"; +} + +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { + const vector<DatatypeType>& datatypes = c->getDatatypes(); + for(vector<DatatypeType>::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); + i != i_end; + ++i) { + out << *i; + } +} + +template <class T> +static bool tryToStream(std::ostream& out, const Command* c) { + if(typeid(*c) == typeid(T)) { + toStream(out, dynamic_cast<const T*>(c)); + return true; + } + return false; +} + }/* CVC4::printer::cvc namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ - diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 410be0571..d794c82e8 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -32,6 +32,7 @@ namespace cvc { class CvcPrinter : public CVC4::Printer { public: void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; };/* class CvcPrinter */ }/* CVC4::printer::cvc namespace */ diff --git a/src/printer/printer.h b/src/printer/printer.h index adbabe3c5..eae2fc48f 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -23,6 +23,7 @@ #include "util/language.h" #include "expr/node.h" +#include "expr/command.h" namespace CVC4 { @@ -45,6 +46,10 @@ public: /** Write a Node out to a stream with this Printer. */ virtual void toStream(std::ostream& out, TNode n, int toDepth, bool types) const = 0; + + /** Write a Command out to a stream with this Printer. */ + virtual void toStream(std::ostream& out, const Command* c, + int toDepth, bool types) const = 0; };/* class Printer */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp index d03cfbbe0..de22a04c1 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt/smt_printer.cpp @@ -17,9 +17,15 @@ **/ #include "printer/smt/smt_printer.h" -#include "util/language.h" +#include "expr/expr.h" // for ExprSetDepth etc.. +#include "util/language.h" // for LANG_AST +#include "expr/node_manager.h" // for VarNameAttr +#include "expr/command.h" #include <iostream> +#include <vector> +#include <string> +#include <typeinfo> using namespace std; @@ -32,6 +38,11 @@ void SmtPrinter::toStream(std::ostream& out, TNode n, n.toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2); }/* SmtPrinter::toStream() */ +void SmtPrinter::toStream(std::ostream& out, const Command* c, + int toDepth, bool types) const { + c->toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2); +}/* SmtPrinter::toStream() */ + }/* CVC4::printer::smt namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h index 8776b1308..058a6b18c 100644 --- a/src/printer/smt/smt_printer.h +++ b/src/printer/smt/smt_printer.h @@ -32,6 +32,7 @@ namespace smt { class SmtPrinter : public CVC4::Printer { public: void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; };/* class SmtPrinter */ }/* CVC4::printer::smt namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 0d5f367ad..5ce571904 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -19,6 +19,9 @@ #include "printer/smt2/smt2_printer.h" #include <iostream> +#include <vector> +#include <string> +#include <typeinfo> using namespace std; @@ -235,6 +238,183 @@ void printBvParameterizedOp(std::ostream& out, TNode n) { out << ")"; } +template <class T> +static bool tryToStream(std::ostream& out, const Command* c); + +void Smt2Printer::toStream(std::ostream& out, const Command* c, + int toDepth, bool types) const { + expr::ExprSetDepth::Scope sdScope(out, toDepth); + expr::ExprPrintTypes::Scope ptScope(out, types); + + if(tryToStream<AssertCommand>(out, c) || + tryToStream<PushCommand>(out, c) || + tryToStream<PopCommand>(out, c) || + tryToStream<CheckSatCommand>(out, c) || + tryToStream<QueryCommand>(out, c) || + tryToStream<QuitCommand>(out, c) || + tryToStream<CommandSequence>(out, c) || + tryToStream<DeclarationCommand>(out, c) || + tryToStream<DefineFunctionCommand>(out, c) || + tryToStream<DefineNamedFunctionCommand>(out, c) || + tryToStream<SimplifyCommand>(out, c) || + tryToStream<GetValueCommand>(out, c) || + tryToStream<GetAssignmentCommand>(out, c) || + tryToStream<GetAssertionsCommand>(out, c) || + tryToStream<SetBenchmarkStatusCommand>(out, c) || + tryToStream<SetBenchmarkLogicCommand>(out, c) || + tryToStream<SetInfoCommand>(out, c) || + tryToStream<GetInfoCommand>(out, c) || + tryToStream<SetOptionCommand>(out, c) || + tryToStream<GetOptionCommand>(out, c) || + tryToStream<DatatypeDeclarationCommand>(out, c)) { + return; + } + + Unhandled("don't know how to print this command as SMT-LIBv2: %s", c->toString().c_str()); + +}/* Smt2Printer::toStream() */ + +static void toStream(std::ostream& out, const AssertCommand* c) { + out << "(assert " << c->getExpr() << ")"; +} + +static void toStream(std::ostream& out, const PushCommand* c) { + out << "(push 1)"; +} + +static void toStream(std::ostream& out, const PopCommand* c) { + out << "(pop 1)"; +} + +static void toStream(std::ostream& out, const CheckSatCommand* c) { + BoolExpr e = c->getExpr(); + if(!e.isNull()) { + out << "(assert " << e << ")"; + } + out << "(check-sat)"; +} + +static void toStream(std::ostream& out, const QueryCommand* c) { + Unhandled("query command"); +} + +static void toStream(std::ostream& out, const QuitCommand* c) { + out << "(exit)"; +} + +static void toStream(std::ostream& out, const CommandSequence* c) { + for(CommandSequence::const_iterator i = c->begin(); + i != c->end(); + ++i) { + out << *i << endl; + } +} + +static void toStream(std::ostream& out, const DeclarationCommand* c) { + const vector<string>& declaredSymbols = c->getDeclaredSymbols(); + Type declaredType = c->getDeclaredType(); + for(vector<string>::const_iterator i = declaredSymbols.begin(); + i != declaredSymbols.end(); + ++i) { + if(declaredType.isFunction()) { + FunctionType ft = declaredType; + out << "(declare-fun " << *i << " ("; + const vector<Type> argTypes = ft.getArgTypes(); + if(argTypes.size() > 0) { + copy( argTypes.begin(), argTypes.end() - 1, + ostream_iterator<Type>(out, " ") ); + out << argTypes.back(); + } + out << ") " << ft.getRangeType() << ")"; + } else { + out << "(declare-fun " << *i << " () " << declaredType << ")"; + } + } +} + +static void toStream(std::ostream& out, const DefineFunctionCommand* c) { + Expr func = c->getFunction(); + const vector<Expr>& formals = c->getFormals(); + Expr formula = c->getFormula(); + out << "(define-fun " << func << " ("; + for(vector<Expr>::const_iterator i = formals.begin(); + i != formals.end(); + ++i) { + out << "(" << (*i) << " " << (*i).getType() << ")"; + } + out << ") " << FunctionType(func.getType()).getRangeType() << " " << formula << ")"; +} + +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { + out << "DefineNamedFunction( "; + toStream(out, static_cast<const DefineFunctionCommand*>(c)); + out << " )"; + Unhandled("define named function command"); +} + +static void toStream(std::ostream& out, const SimplifyCommand* c) { + out << "Simplify( << " << c->getTerm() << " >> )"; + Unhandled("simplify command"); +} + +static void toStream(std::ostream& out, const GetValueCommand* c) { + out << "(get-value " << c->getTerm() << ")"; +} + +static void toStream(std::ostream& out, const GetAssignmentCommand* c) { + out << "(get-assignment)"; +} + +static void toStream(std::ostream& out, const GetAssertionsCommand* c) { + out << "(get-assertions)"; +} + +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) { + out << "(set-info :status " << c->getStatus() << ")"; +} + +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) { + out << "(set-logic " << c->getLogic() << ")"; +} + +static void toStream(std::ostream& out, const SetInfoCommand* c) { + out << "(set-info " << c->getFlag() << " " << c->getSExpr() << ")"; +} + +static void toStream(std::ostream& out, const GetInfoCommand* c) { + out << "(get-info " << c->getFlag() << ")"; +} + +static void toStream(std::ostream& out, const SetOptionCommand* c) { + out << "(set-option " << c->getFlag() << " " << c->getSExpr() << ")"; +} + +static void toStream(std::ostream& out, const GetOptionCommand* c) { + out << "(get-option " << c->getFlag() << ")"; +} + +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { + const vector<DatatypeType>& datatypes = c->getDatatypes(); + out << "DatatypeDeclarationCommand(["; + for(vector<DatatypeType>::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); + i != i_end; + ++i) { + out << *i << ";" << endl; + } + out << "])"; + Unhandled("datatype declaration command"); +} + +template <class T> +static bool tryToStream(std::ostream& out, const Command* c) { + if(typeid(*c) == typeid(T)) { + toStream(out, dynamic_cast<const T*>(c)); + return true; + } + return false; +} + }/* CVC4::printer::smt2 namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 6fce2dfff..4bae8a2e1 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -32,6 +32,7 @@ namespace smt2 { class Smt2Printer : public CVC4::Printer { public: void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; };/* class Smt2Printer */ }/* CVC4::printer::smt2 namespace */ diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 8e98f32c0..0c4f00875 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -240,8 +240,18 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type) if (ps.size() == 0) return ok = false; else if (ps.size() == 1){ - assert(type != CLAUSE_LEMMA); - assert(value(ps[0]) == l_Undef); + if(in_solve) { + assert(type != CLAUSE_LEMMA); + assert(value(ps[0]) == l_Undef); + } else { + // [MGD] at "pre-solve" time we allow unit T-lemmas + if(value(ps[0]) == l_True) { + // this unit T-lemma is extraneous (perhaps it was + // discovered twice at presolve time) + return true; + } + assert(value(ps[0]) == l_Undef); + } uncheckedEnqueue(ps[0]); return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef); }else{ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index cbec9faea..4c9b66020 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -16,9 +16,9 @@ ** Implementation of the propositional engine of CVC4. **/ -#include "cnf_stream.h" -#include "prop_engine.h" -#include "sat.h" +#include "prop/cnf_stream.h" +#include "prop/prop_engine.h" +#include "prop/sat.h" #include "theory/theory_engine.h" #include "theory/registrar.h" @@ -26,6 +26,8 @@ #include "util/options.h" #include "util/output.h" #include "util/result.h" +#include "expr/expr.h" +#include "expr/command.h" #include <utility> #include <map> @@ -88,6 +90,16 @@ void PropEngine::assertLemma(TNode node) { //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; + if(Options::current()->preprocessOnly) { + if(Message.isOn()) { + // If "preprocess only" mode is in effect, the lemmas we get + // here are due to theory reasoning during preprocessing. So + // push the lemma to the Message() stream. + expr::ExprSetDepth::Scope sdScope(Message.getStream(), -1); + Message() << AssertCommand(BoolExpr(node.toExpr())) << endl; + } + } + //TODO This comment is now false // Assert as removable d_cnfStream->convertAndAssert(node, true, false); @@ -124,6 +136,10 @@ Result PropEngine::checkSat() { // TODO This currently ignores conflicts (a dangerous practice). d_theoryEngine->presolve(); + if(Options::current()->preprocessOnly) { + return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK); + } + // Check the problem bool result = d_satSolver->solve(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d85f28b23..fe5628dd0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -669,6 +669,18 @@ void SmtEnginePrivate::processAssertions() { // Simplify the assertions simplifyAssertions(); + if(Options::current()->preprocessOnly) { + if(Message.isOn()) { + // Push the formula to the Message() stream + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + expr::ExprSetDepth::Scope sdScope(Message.getStream(), -1); + Message() << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr())) << endl; + } + } + // We still call into SAT below so that we can output theory + // contributions that come from presolve(). + } + // Push the formula to SAT for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index fa885590b..4237e0992 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -286,6 +286,12 @@ Node TheoryEngine::getValue(TNode node) { }/* TheoryEngine::getValue(TNode node) */ bool TheoryEngine::presolve() { + // NOTE that we don't look at d_theoryIsActive[] here. First of + // all, we haven't done any pre-registration yet, so we don't know + // which theories are active. Second, let's give each theory a shot + // at doing something with the input formula, even if it wouldn't + // otherwise be active. + d_theoryOut.d_conflictNode = Node::null(); d_theoryOut.d_propagatedLiterals.clear(); @@ -295,7 +301,7 @@ bool TheoryEngine::presolve() { #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasPresolve && d_theoryIsActive[THEORY]) { \ + if (theory::TheoryTraits<THEORY>::hasPresolve) { \ reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->presolve(); \ if(!d_theoryOut.d_conflictNode.get().isNull()) { \ return true; \ diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 8527924da..fc0f32927 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -15,7 +15,9 @@ libuf_la_SOURCES = \ theory_uf_type_rules.h \ theory_uf_rewriter.h \ equality_engine.h \ - equality_engine_impl.h + equality_engine_impl.h \ + symmetry_breaker.h \ + symmetry_breaker.cpp libuf_la_LIBADD = \ @builddir@/tim/libuftim.la \ diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index e15467bff..01bab53ac 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -20,6 +20,7 @@ #include "theory/valuation.h" #include "expr/kind.h" #include "util/congruence_closure.h" +#include "theory/uf/symmetry_breaker.h" #include <map> @@ -559,6 +560,15 @@ void TheoryUFMorgan::presolve() { TimerStat::CodeTimer codeTimer(d_presolveTimer); Debug("uf") << "uf: begin presolve()" << endl; + if(Options::current()->ufSymmetryBreaker) { + vector<Node> newClauses; + d_symb.apply(newClauses); + for(vector<Node>::const_iterator i = newClauses.begin(); + i != newClauses.end(); + ++i) { + d_out->lemma(*i); + } + } Debug("uf") << "uf: end presolve()" << endl; } @@ -699,6 +709,10 @@ void TheoryUFMorgan::staticLearning(TNode n, NodeBuilder<>& learned) { } } } + + if(Options::current()->ufSymmetryBreaker) { + d_symb.assertFormula(n); + } } /* diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index c2feef349..e801f383e 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -31,6 +31,7 @@ #include "theory/theory.h" #include "theory/uf/theory_uf.h" #include "theory/uf/morgan/union_find.h" +#include "theory/uf/symmetry_breaker.h" #include "context/context.h" #include "context/context_mm.h" @@ -66,6 +67,8 @@ private: */ context::CDList<Node> d_assertions; + SymmetryBreaker d_symb; + /** * Our channel connected to the congruence closure module. */ diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp new file mode 100644 index 000000000..1c2e8cd0d --- /dev/null +++ b/src/theory/uf/symmetry_breaker.cpp @@ -0,0 +1,616 @@ +/********************* */ +/*! \file symmetry_breaker.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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.\endverbatim + ** + ** \brief Implementation of algorithm suggested by Deharbe, Fontaine, + ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011 + ** + ** Implementation of algorithm suggested by Deharbe, Fontaine, Merz, + ** and Paleo, "Exploiting symmetry in SMT problems," CADE 2011. + ** + ** From the paper: + ** + ** <pre> + ** P := guess_permutations(phi) + ** foreach {c_0, ..., c_n} \in P do + ** if invariant_by_permutations(phi, {c_0, ..., c_n}) then + ** T := select_terms(phi, {c_0, ..., c_n}) + ** cts := \empty + ** while T != \empty && |cts| <= n do + ** t := select_most_promising_term(T, phi) + ** T := T \ {t} + ** cts := cts \cup used_in(t, {c_0, ..., c_n}) + ** let c \in {c_0, ..., c_n} \ cts + ** cts := cts \cup {c} + ** if cts != {c_0, ..., c_n} then + ** phi := phi /\ ( \vee_{c_i \in cts} t = c_i ) + ** end + ** end + ** end + ** end + ** return phi + ** </pre> + **/ + +#include "theory/uf/symmetry_breaker.h" +#include "theory/rewriter.h" +#include "util/hash.h" + +#include <iterator> +#include <queue> + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace uf { + +SymmetryBreaker::Template::Template() : + d_template(), + d_sets(), + d_reps() { +} + +TNode SymmetryBreaker::Template::find(TNode n) { + hash_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n); + if(i == d_reps.end()) { + return n; + } else { + return d_reps[n] = find((*i).second); + } +} + +bool SymmetryBreaker::Template::matchRecursive(TNode t, TNode n) { + IndentedScope scope(Debug("ufsymm:match")); + + Debug("ufsymm:match") << "UFSYMM matching " << t << endl + << "UFSYMM to " << n << endl; + + if(t.getKind() != n.getKind() || t.getNumChildren() != n.getNumChildren()) { + Debug("ufsymm:match") << "UFSYMM BAD MATCH on kind, #children" << endl; + return false; + } + + if(t.getNumChildren() == 0) { + if(t.getMetaKind() == kind::metakind::CONSTANT) { + Assert(n.getMetaKind() == kind::metakind::CONSTANT); + Debug("ufsymm:match") << "UFSYMM we have constants, failing match" << endl; + return false; + } + Assert(t.getMetaKind() == kind::metakind::VARIABLE && + n.getMetaKind() == kind::metakind::VARIABLE); + t = find(t); + n = find(n); + Debug("ufsymm:match") << "UFSYMM variable match " << t << " , " << n << endl; + Debug("ufsymm:match") << "UFSYMM sets: " << t << " =>"; + if(d_sets.find(t) != d_sets.end()) { + for(set<TNode>::iterator i = d_sets[t].begin(); i != d_sets[t].end(); ++i) { + Debug("ufsymm:match") << " " << *i; + } + } + Debug("ufsymm:match") << endl; + if(t != n) { + Debug("ufsymm:match") << "UFSYMM sets: " << n << " =>"; + if(d_sets.find(n) != d_sets.end()) { + for(set<TNode>::iterator i = d_sets[n].begin(); i != d_sets[n].end(); ++i) { + Debug("ufsymm:match") << " " << *i; + } + } + Debug("ufsymm:match") << endl; + + if(d_sets.find(t) == d_sets.end()) { + Debug("ufsymm:match") << "UFSYMM inserting " << t << " in with " << n << endl; + d_reps[t] = n; + d_sets[n].insert(t); + } else { + if(d_sets.find(n) != d_sets.end()) { + Debug("ufsymm:match") << "UFSYMM merging " << n << " and " << t << " in with " << n << endl; + d_sets[n].insert(d_sets[t].begin(), d_sets[t].end()); + d_sets[n].insert(t); + d_reps[t] = n; + d_sets.erase(t); + } else { + Debug("ufsymm:match") << "UFSYMM inserting " << n << " in with " << t << endl; + d_sets[t].insert(n); + d_reps[n] = t; + } + } + } + return true; + } + + if(t.getMetaKind() == kind::metakind::PARAMETERIZED) { + if(t.getOperator() != n.getOperator()) { + Debug("ufsymm:match") << "UFSYMM BAD MATCH on operators: " << t.getOperator() << " != " << n.getOperator() << endl; + return false; + } + } + TNode::iterator ti = t.begin(); + TNode::iterator ni = n.begin(); + while(ti != t.end()) { + if(*ti != *ni) { // nothing to do if equal + if(!matchRecursive(*ti, *ni)) { + Debug("ufsymm:match") << "UFSYMM BAD MATCH, withdrawing.." << endl; + return false; + } + } + ++ti; + ++ni; + } + + return true; +} + +bool SymmetryBreaker::Template::match(TNode n) { + // try to "match" n and d_template + if(d_template.isNull()) { + Debug("ufsymm") << "UFSYMM setting template " << n << endl; + d_template = n; + return true; + } else { + return matchRecursive(d_template, n); + } +} + +void SymmetryBreaker::Template::reset() { + d_template = Node::null(); + d_sets.clear(); + d_reps.clear(); +} + +SymmetryBreaker::SymmetryBreaker() : + d_phi(), + d_phiSet(), + d_permutations(), + d_terms(), + d_template(), + d_normalizationCache(), + d_termEqs() { +} + +Node SymmetryBreaker::norm(TNode phi) { + Node n = Rewriter::rewrite(phi); + return normInternal(n); +} + +Node SymmetryBreaker::normInternal(TNode n) { + Node& result = d_normalizationCache[n]; + if(!result.isNull()) { + return result; + } + + switch(Kind k = n.getKind()) { + + case kind::DISTINCT: { + // commutative N-ary operator handling + vector<TNode> kids(n.begin(), n.end()); + sort(kids.begin(), kids.end()); + return result = NodeManager::currentNM()->mkNode(k, kids); + } + + case kind::AND: + case kind::OR: { + // commutative+associative N-ary operator handling + vector<Node> kids; + kids.reserve(n.getNumChildren()); + queue<TNode> work; + work.push(n); + Debug("ufsymm:norm") << "UFSYMM processing " << n << endl; + do { + TNode m = work.front(); + work.pop(); + for(TNode::iterator i = m.begin(); i != m.end(); ++i) { + if((*i).getKind() == k) { + work.push(*i); + } else { + if( (*i).getKind() == kind::AND || + (*i).getKind() == kind::OR ) { + kids.push_back(normInternal(*i)); + } else if((*i).getKind() == kind::IFF || + (*i).getKind() == kind::EQUAL) { + kids.push_back(normInternal(*i)); + if((*i)[0].getMetaKind() == kind::metakind::VARIABLE || + (*i)[1].getMetaKind() == kind::metakind::VARIABLE) { + d_termEqs[(*i)[0]].insert((*i)[1]); + d_termEqs[(*i)[1]].insert((*i)[0]); + Debug("ufsymm:eq") << "UFSYMM " << (*i)[0] << " <==> " << (*i)[1] << endl; + } + } else { + kids.push_back(*i); + } + } + } + } while(!work.empty()); + Debug("ufsymm:norm") << "UFSYMM got " << kids.size() << " kids for the " << k << "-kinded Node" << endl; + sort(kids.begin(), kids.end()); + return result = NodeManager::currentNM()->mkNode(k, kids); + } + + case kind::IFF: + case kind::EQUAL: + if(n[0].getMetaKind() == kind::metakind::VARIABLE || + n[1].getMetaKind() == kind::metakind::VARIABLE) { + d_termEqs[n[0]].insert(n[1]); + d_termEqs[n[1]].insert(n[0]); + Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl; + } + /* intentional fall-through! */ + case kind::XOR: + // commutative binary operator handling + return n[1] < n[0] ? NodeManager::currentNM()->mkNode(k, n[1], n[0]) : Node(n); + + default: + // Normally T-rewriting is enough; only special cases (like + // Boolean-layer stuff) has to go above. + return n; + } +} + +void SymmetryBreaker::assertFormula(TNode phi) { + // use d_phi, put into d_permutations + Debug("ufsymm") << "UFSYMM assertFormula(): phi is " << phi << endl; + d_phi.push_back(phi); + if(phi.getKind() == kind::OR) { + Template t; + Node::iterator i = phi.begin(); + t.match(*i++); + while(i != phi.end()) { + if(!t.match(*i++)) { + break; + } + } + hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions(); + for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); + i != ps.end(); + ++i) { + Debug("ufsymm") << "UFSYMM partition*: " << (*i).first; + set<TNode>& p = (*i).second; + for(set<TNode>::iterator j = p.begin(); + j != p.end(); + ++j) { + Debug("ufsymm") << " " << *j; + } + Debug("ufsymm") << endl; + p.insert((*i).first); + Permutations::iterator pi = d_permutations.find(p); + if(pi == d_permutations.end()) { + d_permutations.insert(p); + } + } + } + if(!d_template.match(phi)) { + // we hit a bad match, extract the partitions and reset the template + hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions(); + Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl; + for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); + i != ps.end(); + ++i) { + Debug("ufsymm") << "UFSYMM partition: " << (*i).first; + set<TNode>& p = (*i).second; + if(Debug.isOn("ufsymm")) { + for(set<TNode>::iterator j = p.begin(); + j != p.end(); + ++j) { + Debug("ufsymm") << " " << *j; + } + } + Debug("ufsymm") << endl; + p.insert((*i).first); + d_permutations.insert(p); + } + d_template.reset(); + bool good CVC4_UNUSED = d_template.match(phi); + Assert(good); + } +} + +void SymmetryBreaker::clear() { + d_phi.clear(); + d_phiSet.clear(); + d_permutations.clear(); + d_terms.clear(); + d_template.reset(); + d_normalizationCache.clear(); + d_termEqs.clear(); +} + +void SymmetryBreaker::apply(std::vector<Node>& newClauses) { + guessPermutations(); + Debug("ufsymm") << "UFSYMM =====================================================" << endl + << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl; + if(!d_permutations.empty()) { + { TimerStat::CodeTimer codeTimer(d_initNormalizationTimer); + // normalize d_phi + + for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { + Node n = *i; + *i = norm(n); + d_phiSet.insert(*i); + Debug("ufsymm:norm") << "UFSYMM init-norm-rewrite " << n << endl + << "UFSYMM to " << *i << endl; + } + } + + for(Permutations::iterator i = d_permutations.begin(); + i != d_permutations.end(); + ++i) { + ++d_permutationSetsConsidered; + const Permutation& p = *i; + Debug("ufsymm") << "UFSYMM looking at permutation: " << p << endl; + size_t n = p.size() - 1; + if(invariantByPermutations(p)) { + ++d_permutationSetsInvariant; + selectTerms(p); + set<Node> cts; + while(!d_terms.empty() && cts.size() <= n) { + Debug("ufsymm") << "UFSYMM ==== top of loop, d_terms.size() == " << d_terms.size() << " , cts.size() == " << cts.size() << " , n == " << n << endl; + Terms::iterator ti = selectMostPromisingTerm(d_terms); + Node t = *ti; + Debug("ufsymm") << "UFSYMM promising term is " << t << endl; + d_terms.erase(ti); + insertUsedIn(t, p, cts); + if(Debug.isOn("ufsymm")) { + if(cts.empty()) { + Debug("ufsymm") << "UFSYMM cts is empty" << endl; + } else { + for(set<Node>::iterator ctsi = cts.begin(); ctsi != cts.end(); ++ctsi) { + Debug("ufsymm") << "UFSYMM cts: " << *ctsi << endl; + } + } + } + TNode c; + Debug("ufsymm") << "UFSYMM looking for c \\in " << p << " \\ cts" << endl; + set<TNode>::const_iterator i; + for(i = p.begin(); i != p.end(); ++i) { + if(cts.find(*i) == cts.end()) { + if(c.isNull()) { + c = *i; + Debug("ufsymm") << "UFSYMM found first: " << c << endl; + } else { + Debug("ufsymm") << "UFSYMM found second: " << *i << endl; + break; + } + } + } + if(c.isNull()) { + Debug("ufsymm") << "UFSYMM can't find a c, restart outer loop" << endl; + break; + } + Debug("ufsymm") << "UFSYMM inserting into cts: " << c << endl; + cts.insert(c); + // This tests cts != p: if "i == p.end()", we got all the way + // through p without seeing two elements not in cts (on the + // second one, we break from the above loop). We know we + // found at least one (and subsequently added it to cts). So + // now cts == p. + Debug("ufsymm") << "UFSYMM p == " << p << endl; + if(i != p.end() || p.size() != cts.size()) { + Debug("ufsymm") << "UFSYMM cts != p" << endl; + NodeBuilder<> disj(kind::OR); + for(set<Node>::const_iterator i = cts.begin(); + i != cts.end(); + ++i) { + if(t != *i) { + disj << NodeManager::currentNM()->mkNode(kind::EQUAL, t, *i); + } + } + Node d; + if(disj.getNumChildren() > 1) { + d = disj; + ++d_clauses; + } else { + d = disj[0]; + disj.clear(); + ++d_units; + } + if(Debug.isOn("ufsymm")) { + Debug("ufsymm") << "UFSYMM symmetry-breaking clause: " << d << endl; + } else { + Debug("ufsymm:clauses") << "UFSYMM symmetry-breaking clause: " << d << endl; + } + newClauses.push_back(d); + } else { + Debug("ufsymm") << "UFSYMM cts == p" << endl; + } + Debug("ufsymm") << "UFSYMM ==== end of loop, d_terms.size() == " << d_terms.size() << " , cts.size() == " << cts.size() << " , n == " << n << endl; + } + } + } + } + + clear(); +} + +void SymmetryBreaker::guessPermutations() { + // use d_phi, put into d_permutations + Debug("ufsymm") << "UFSYMM guessPermutations()" << endl; +} + +bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { + TimerStat::CodeTimer codeTimer(d_invariantByPermutationsTimer); + + // use d_phi + Debug("ufsymm") << "UFSYMM invariantByPermutations()? " << p << endl; + + Assert(p.size() > 1); + + // check P_swap + vector<Node> subs; + vector<Node> repls; + Permutation::iterator i = p.begin(); + TNode p0 = *i++; + TNode p1 = *i; + subs.push_back(p0); + subs.push_back(p1); + repls.push_back(p1); + repls.push_back(p0); + for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { + Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); + Node n = norm(s); + if(*i != n && d_phiSet.find(n) == d_phiSet.end()) { + Debug("ufsymm") << "UFSYMM P_swap is NOT an inv perm op for " << p << endl + << "UFSYMM because this node: " << *i << endl + << "UFSYMM rewrite-norms to : " << n << endl + << "UFSYMM which is not in our set of normalized assertions" << endl; + return false; + } else if(Debug.isOn("ufsymm:p")) { + if(*i == s) { + Debug("ufsymm:p") << "UFSYMM P_swap passes trivially: " << *i << endl; + } else { + Debug("ufsymm:p") << "UFSYMM P_swap passes: " << *i << endl + << "UFSYMM rewrites: " << s << endl + << "UFSYMM norms: " << n << endl; + } + } + } + Debug("ufsymm") << "UFSYMM P_swap is an inv perm op for " << p << endl; + + // check P_circ, unless size == 2 in which case P_circ == P_swap + if(p.size() > 2) { + subs.clear(); + repls.clear(); + bool first = true; + for(Permutation::const_iterator i = p.begin(); i != p.end(); ++i) { + subs.push_back(*i); + if(!first) { + repls.push_back(*i); + } else { + first = false; + } + } + repls.push_back(*p.begin()); + Assert(subs.size() == repls.size()); + for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { + Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); + Node n = norm(s); + if(*i != n && d_phiSet.find(n) == d_phiSet.end()) { + Debug("ufsymm") << "UFSYMM P_circ is NOT an inv perm op for " << p << endl + << "UFSYMM because this node: " << *i << endl + << "UFSYMM rewrite-norms to : " << n << endl + << "UFSYMM which is not in our set of normalized assertions" << endl; + return false; + } else if(Debug.isOn("ufsymm:p")) { + if(*i == s) { + Debug("ufsymm:p") << "UFSYMM P_circ passes trivially: " << *i << endl; + } else { + Debug("ufsymm:p") << "UFSYMM P_circ passes: " << *i << endl + << "UFSYMM rewrites: " << s << endl + << "UFSYMM norms: " << n << endl; + } + } + } + Debug("ufsymm") << "UFSYMM P_circ is an inv perm op for " << p << endl; + } else { + Debug("ufsymm") << "UFSYMM no need to check P_circ, since P_circ == P_swap for perm sets of size 2" << endl; + } + + return true; +} + +// debug-assertion-only function +template <class T1, class T2> +static bool isSubset(const T1& s, const T2& t) { + if(s.size() > t.size()) { + //Debug("ufsymm") << "DEBUG ASSERTION FAIL: s not a subset of t " + // << "because size(s) > size(t)" << endl; + return false; + } + for(typename T1::const_iterator si = s.begin(); si != s.end(); ++si) { + if(t.find(*si) == t.end()) { + //Debug("ufsymm") << "DEBUG ASSERTION FAIL: s not a subset of t " + // << "because s element \"" << *si << "\" not in t" << endl; + return false; + } + } + + // At this point, didn't find any elements from s not in t, so + // conclude that s \subseteq t + return true; +} + +void SymmetryBreaker::selectTerms(const Permutation& p) { + TimerStat::CodeTimer codeTimer(d_selectTermsTimer); + + // use d_phi, put into d_terms + Debug("ufsymm") << "UFSYMM selectTerms(): " << p << endl; + d_terms.clear(); + set<Node> terms; + for(Permutation::iterator i = p.begin(); i != p.end(); ++i) { + const TermEq& teq = d_termEqs[*i]; + terms.insert(teq.begin(), teq.end()); + } + for(set<Node>::iterator i = terms.begin(); i != terms.end(); ++i) { + const TermEq& teq = d_termEqs[*i]; + if(isSubset(teq, p)) { + d_terms.insert(d_terms.end(), *i); + } else { + if(Debug.isOn("ufsymm")) { + Debug("ufsymm") << "UFSYMM selectTerms() threw away candidate: " << *i << endl; + Debug("ufsymm:eq") << "UFSYMM selectTerms() #teq == " << teq.size() << " #p == " << p.size() << endl; + TermEq::iterator j; + for(j = teq.begin(); j != teq.end(); ++j) { + Debug("ufsymm:eq") << "UFSYMM -- teq " << *j << " in " << p << " ?" << endl; + if(p.find(*j) == p.end()) { + Debug("ufsymm") << "UFSYMM -- because its teq " << *j + << " isn't in " << p << endl; + break; + } else { + Debug("ufsymm:eq") << "UFSYMM -- yep" << endl; + } + } + Assert(j != teq.end(), "failed to find a difference between p and teq ?!"); + } + } + } + if(Debug.isOn("ufsymm")) { + for(list<Term>::iterator i = d_terms.begin(); i != d_terms.end(); ++i) { + Debug("ufsymm") << "UFSYMM selectTerms() returning: " << *i << endl; + } + } +} + +SymmetryBreaker::Terms::iterator +SymmetryBreaker::selectMostPromisingTerm(Terms& terms) { + // use d_phi + Debug("ufsymm") << "UFSYMM selectMostPromisingTerm()" << endl; + return terms.begin(); +} + +void SymmetryBreaker::insertUsedIn(Term term, const Permutation& p, set<Node>& cts) { + // insert terms from p used in term into cts + //Debug("ufsymm") << "UFSYMM usedIn(): " << term << " , " << p << endl; + if(find(p.begin(), p.end(), term) != p.end()) { + cts.insert(term); + } else { + for(TNode::iterator i = term.begin(); i != term.end(); ++i) { + insertUsedIn(*i, p, cts); + } + } +} + +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, const theory::uf::SymmetryBreaker::Permutation& p) { + out << "{"; + set<TNode>::const_iterator i = p.begin(); + while(i != p.end()) { + out << *i; + if(++i != p.end()) { + out << ","; + } + } + out << "}"; + return out; +} + +}/* CVC4 namespace */ diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h new file mode 100644 index 000000000..1b2680cf3 --- /dev/null +++ b/src/theory/uf/symmetry_breaker.h @@ -0,0 +1,160 @@ +/********************* */ +/*! \file symmetry_breaker.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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.\endverbatim + ** + ** \brief Implementation of algorithm suggested by Deharbe, Fontaine, + ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011 + ** + ** Implementation of algorithm suggested by Deharbe, Fontaine, + ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011. + ** + ** From the paper: + ** + ** <pre> + ** P := guess_permutations(phi) + ** foreach {c_0, ..., c_n} \in P do + ** if invariant_by_permutations(phi, {c_0, ..., c_n}) then + ** T := select_terms(phi, {c_0, ..., c_n}) + ** cts := \empty + ** while T != \empty && |cts| <= n do + ** t := select_most_promising_term(T, phi) + ** T := T \ {t} + ** cts := cts \cup used_in(t, {c_0, ..., c_n}) + ** let c \in {c_0, ..., c_n} \ cts + ** cts := cts \cup {c} + ** if cts != {c_0, ..., c_n} then + ** phi := phi /\ ( \vee_{c_i \in cts} t = c_i ) + ** end + ** end + ** end + ** end + ** return phi + ** </pre> + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__UF__SYMMETRY_BREAKER_H +#define __CVC4__THEORY__UF__SYMMETRY_BREAKER_H + +#include <iostream> +#include <list> +#include <vector> + +#include "expr/node.h" +#include "expr/node_builder.h" +#include "util/stats.h" + +namespace CVC4 { +namespace theory { +namespace uf { + +class SymmetryBreaker { + + class Template { + Node d_template; + NodeBuilder<> d_assertions; + std::hash_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets; + std::hash_map<TNode, TNode, TNodeHashFunction> d_reps; + + TNode find(TNode n); + bool matchRecursive(TNode t, TNode n); + + public: + Template(); + bool match(TNode n); + std::hash_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; } + Node assertions() { + switch(d_assertions.getNumChildren()) { + case 0: return Node::null(); + case 1: return d_assertions[0]; + default: return Node(d_assertions); + } + } + void reset(); + };/* class SymmetryBreaker::Template */ + +public: + + typedef std::set<TNode> Permutation; + typedef std::set<Permutation> Permutations; + typedef TNode Term; + typedef std::list<Term> Terms; + typedef std::set<Term> TermEq; + typedef std::hash_map<Term, TermEq, TNodeHashFunction> TermEqs; + +private: + + std::vector<Node> d_phi; + std::set<TNode> d_phiSet; + Permutations d_permutations; + Terms d_terms; + Template d_template; + std::hash_map<Node, Node, NodeHashFunction> d_normalizationCache; + TermEqs d_termEqs; + + void clear(); + + void guessPermutations(); + bool invariantByPermutations(const Permutation& p); + void selectTerms(const Permutation& p); + Terms::iterator selectMostPromisingTerm(Terms& terms); + void insertUsedIn(Term term, const Permutation& p, std::set<Node>& cts); + Node normInternal(TNode phi); + Node norm(TNode n); + + // === STATISTICS === + /** number of new clauses that come from the SymmetryBreaker */ + KEEP_STATISTIC(IntStat, + d_clauses, + "theory::uf::symmetry_breaker::clauses", 0); + /** number of new clauses that come from the SymmetryBreaker */ + KEEP_STATISTIC(IntStat, + d_units, + "theory::uf::symmetry_breaker::units", 0); + /** number of potential permutation sets we found */ + KEEP_STATISTIC(IntStat, + d_permutationSetsConsidered, + "theory::uf::symmetry_breaker::permutationSetsConsidered", 0); + /** number of invariant permutation sets we found */ + KEEP_STATISTIC(IntStat, + d_permutationSetsInvariant, + "theory::uf::symmetry_breaker::permutationSetsInvariant", 0); + /** time spent in invariantByPermutations() */ + KEEP_STATISTIC(TimerStat, + d_invariantByPermutationsTimer, + "theory::uf::symmetry_breaker::timers::invariantByPermutations"); + /** time spent in selectTerms() */ + KEEP_STATISTIC(TimerStat, + d_selectTermsTimer, + "theory::uf::symmetry_breaker::timers::selectTerms"); + /** time spent in initial round of normalization */ + KEEP_STATISTIC(TimerStat, + d_initNormalizationTimer, + "theory::uf::symmetry_breaker::timers::initNormalization"); + +public: + + SymmetryBreaker(); + void assertFormula(TNode phi); + void apply(std::vector<Node>& newClauses); + +};/* class SymmetryBreaker */ + +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, const ::CVC4::theory::uf::SymmetryBreaker::Permutation& p); + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__UF__SYMMETRY_BREAKER_H */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9903acc57..0776ecf0d 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -227,6 +227,22 @@ void TheoryUF::explain(TNode literal) { d_out->explanation(mkAnd(assumptions)); } +void TheoryUF::presolve() { + // TimerStat::CodeTimer codeTimer(d_presolveTimer); + + Debug("uf") << "uf: begin presolve()" << endl; + if(Options::current()->ufSymmetryBreaker) { + vector<Node> newClauses; + d_symb.apply(newClauses); + for(vector<Node>::const_iterator i = newClauses.begin(); + i != newClauses.end(); + ++i) { + d_out->lemma(*i); + } + } + Debug("uf") << "uf: end presolve()" << endl; +} + void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) { //TimerStat::CodeTimer codeTimer(d_staticLearningTimer); @@ -334,4 +350,8 @@ void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) { } } } + + if(Options::current()->ufSymmetryBreaker) { + d_symb.assertFormula(n); + } } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index eaab96f27..d78504dc8 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -27,6 +27,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" +#include "theory/uf/symmetry_breaker.h" #include "context/cdo.h" #include "context/cdset.h" @@ -87,6 +88,9 @@ private: /** True node for predicates = false */ Node d_false; + /** Symmetry analyzer */ + SymmetryBreaker d_symb; + public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ @@ -113,12 +117,13 @@ public: void preRegisterTerm(TNode term); void explain(TNode n); + void staticLearning(TNode in, NodeBuilder<>& learned); + void presolve(); + std::string identify() const { return "THEORY_UF"; } - void staticLearning(TNode in, NodeBuilder<>& learned); - };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ diff --git a/src/util/options.cpp b/src/util/options.cpp index ff028b6c6..9bceee931 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -88,7 +88,8 @@ Options::Options() : satRandomSeed(91648253),// Minisat's default value pivotRule(MINIMUM), arithPivotThreshold(16), - arithPropagateMaxLength(16) + arithPropagateMaxLength(16), + ufSymmetryBreaker(true) { } @@ -97,6 +98,7 @@ static const string optionsDescription = "\ --version | -V identify this CVC4 binary\n\ --help | -h this command line reference\n\ --parse-only exit after parsing input\n\ + --preprocess-only exit after parsing preprocessing input (and dump preprocessed assertions, unless -q)\n\ --mmap memory map file input\n\ --show-config show CVC4 static configuration\n\ --segv-nospin don't spin on segfault waiting for gdb\n\ @@ -129,6 +131,7 @@ static const string optionsDescription = "\ --random-seed=S sets the random seed for the sat solver\n\ --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ --disable-arithmetic-propagation turns on arithmetic propagation\n\ + --disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\ --incremental enable incremental solving\n"; static const string languageDescription = "\ @@ -190,6 +193,7 @@ enum OptionValue { STATS, SEGV_NOSPIN, PARSE_ONLY, + PREPROCESS_ONLY, NO_CHECKING, NO_THEORY_REGISTRATION, USE_MMAP, @@ -216,7 +220,8 @@ enum OptionValue { ARITHMETIC_VARIABLE_REMOVAL, ARITHMETIC_PROPAGATION, ARITHMETIC_PIVOT_THRESHOLD, - ARITHMETIC_PROP_MAX_LENGTH + ARITHMETIC_PROP_MAX_LENGTH, + DISABLE_SYMMETRY_BREAKER };/* enum OptionValue */ /** @@ -259,6 +264,7 @@ static struct option cmdlineOptions[] = { { "about" , no_argument , NULL, 'V' }, { "lang" , required_argument, NULL, 'L' }, { "parse-only" , no_argument , NULL, PARSE_ONLY }, + { "preprocess-only", no_argument , NULL, PREPROCESS_ONLY }, { "mmap" , no_argument , NULL, USE_MMAP }, { "strict-parsing", no_argument , NULL, STRICT_PARSING }, { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH }, @@ -288,6 +294,7 @@ static struct option cmdlineOptions[] = { { "random-seed" , required_argument, NULL, RANDOM_SEED }, { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL }, { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, + { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER }, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -385,6 +392,10 @@ throw(OptionException) { parseOnly = true; break; + case PREPROCESS_ONLY: + preprocessOnly = true; + break; + case NO_THEORY_REGISTRATION: theoryRegistration = false; break; @@ -542,6 +553,10 @@ throw(OptionException) { arithPropagation = false; break; + case DISABLE_SYMMETRY_BREAKER: + ufSymmetryBreaker = false; + break; + case RANDOM_SEED: satRandomSeed = atof(optarg); break; diff --git a/src/util/options.h b/src/util/options.h index 06ca20073..ce2bc71e7 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -89,6 +89,9 @@ struct CVC4_PUBLIC Options { /** Should we exit after parsing? */ bool parseOnly; + /** Should we exit after preprocessing? */ + bool preprocessOnly; + /** Should the parser do semantic checks? */ bool semanticChecks; @@ -194,6 +197,12 @@ struct CVC4_PUBLIC Options { */ uint16_t arithPropagateMaxLength; + /** + * Whether to do the symmetry-breaking preprocessing in UF as + * described by Deharbe et al. in CADE 2011 (on by default). + */ + bool ufSymmetryBreaker; + Options(); /** |