#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;
}
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 {
}
/* empty commands have no implementation */
}
-void EmptyCommand::toStream(std::ostream& out) const {
- out << "EmptyCommand(" << d_name << ")";
-}
-
/* class AssertCommand */
AssertCommand::AssertCommand(const BoolExpr& e) :
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) :
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;
}
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() :
}
}
-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) :
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,
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,
}
}
-void DefineNamedFunctionCommand::toStream(std::ostream& out) const {
- out << "DefineNamedFunction( ";
- this->DefineFunctionCommand::toStream(out);
- out << " )";
-}
-
/* class Simplify */
SimplifyCommand::SimplifyCommand(Expr term) :
}
void SimplifyCommand::invoke(SmtEngine* smtEngine) {
-#warning TODO: what is this
+ d_result = smtEngine->simplify(d_term);
}
Expr SimplifyCommand::getResult() const {
out << d_result << endl;
}
-void SimplifyCommand::toStream(std::ostream& out) const {
- out << "Simplify( << " << d_term << " >> )";
-}
-
/* class GetValueCommand */
GetValueCommand::GetValueCommand(Expr term) :
out << d_result << endl;
}
-void GetValueCommand::toStream(std::ostream& out) const {
- out << "GetValue( << " << d_term << " >> )";
-}
-
/* class GetAssignmentCommand */
GetAssignmentCommand::GetAssignmentCommand() {
out << d_result << endl;
}
-void GetAssignmentCommand::toStream(std::ostream& out) const {
- out << "GetAssignment()";
-}
-
/* class GetAssertionsCommand */
GetAssertionsCommand::GetAssertionsCommand() {
out << d_result;
}
-void GetAssertionsCommand::toStream(std::ostream& out) const {
- out << "GetAssertions()";
-}
-
/* class SetBenchmarkStatusCommand */
SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
}
}
-void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
- out << "SetBenchmarkStatus(" << d_status << ")";
-}
-
/* class SetBenchmarkLogicCommand */
SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) :
}
}
-void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
- out << "SetBenchmarkLogic(" << d_logic << ")";
-}
-
/* class SetInfoCommand */
SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) :
}
}
-void SetInfoCommand::toStream(std::ostream& out) const {
- out << "SetInfo(" << d_flag << ", " << d_sexpr << ")";
-}
-
/* class GetInfoCommand */
GetInfoCommand::GetInfoCommand(std::string flag) :
}
}
-void GetInfoCommand::toStream(std::ostream& out) const {
- out << "GetInfo(" << d_flag << ")";
-}
-
/* class SetOptionCommand */
SetOptionCommand::SetOptionCommand(std::string flag, SExpr& sexpr) :
}
}
-void SetOptionCommand::toStream(std::ostream& out) const {
- out << "SetOption(" << d_flag << ", " << d_sexpr << ")";
-}
-
/* class GetOptionCommand */
GetOptionCommand::GetOptionCommand(std::string flag) :
}
}
-void GetOptionCommand::toStream(std::ostream& out) const {
- out << "GetOption(" << d_flag << ")";
-}
-
/* class DatatypeDeclarationCommand */
DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) :
//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) {
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 */
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 {
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 {
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 {
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 */
/**
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 {
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 {
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
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 {
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 {
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 {
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 {
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 {
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 {
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 */
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 */
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 */
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 */
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 {
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;
**/
#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;
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";
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 */
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 */
**/
#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>
}/* 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 */
-
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 */
#include "util/language.h"
#include "expr/node.h"
+#include "expr/command.h"
namespace CVC4 {
/** 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 */
**/
#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;
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 */
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 */
#include "printer/smt2/smt2_printer.h"
#include <iostream>
+#include <vector>
+#include <string>
+#include <typeinfo>
using namespace std;
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 */
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 */
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{
** 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"
#include "util/options.h"
#include "util/output.h"
#include "util/result.h"
+#include "expr/expr.h"
+#include "expr/command.h"
#include <utility>
#include <map>
//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);
// 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();
// 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]);
}/* 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();
#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; \
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 \
#include "theory/valuation.h"
#include "expr/kind.h"
#include "util/congruence_closure.h"
+#include "theory/uf/symmetry_breaker.h"
#include <map>
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;
}
}
}
}
+
+ if(Options::current()->ufSymmetryBreaker) {
+ d_symb.assertFormula(n);
+ }
}
/*
#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"
*/
context::CDList<Node> d_assertions;
+ SymmetryBreaker d_symb;
+
/**
* Our channel connected to the congruence closure module.
*/
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
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);
}
}
}
+
+ if(Options::current()->ufSymmetryBreaker) {
+ d_symb.assertFormula(n);
+ }
}
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
+#include "theory/uf/symmetry_breaker.h"
#include "context/cdo.h"
#include "context/cdset.h"
/** 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.*/
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 */
satRandomSeed(91648253),// Minisat's default value
pivotRule(MINIMUM),
arithPivotThreshold(16),
- arithPropagateMaxLength(16)
+ arithPropagateMaxLength(16),
+ ufSymmetryBreaker(true)
{
}
--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\
--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 = "\
STATS,
SEGV_NOSPIN,
PARSE_ONLY,
+ PREPROCESS_ONLY,
NO_CHECKING,
NO_THEORY_REGISTRATION,
USE_MMAP,
ARITHMETIC_VARIABLE_REMOVAL,
ARITHMETIC_PROPAGATION,
ARITHMETIC_PIVOT_THRESHOLD,
- ARITHMETIC_PROP_MAX_LENGTH
+ ARITHMETIC_PROP_MAX_LENGTH,
+ DISABLE_SYMMETRY_BREAKER
};/* enum OptionValue */
/**
{ "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 },
{ "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! */
parseOnly = true;
break;
+ case PREPROCESS_ONLY:
+ preprocessOnly = true;
+ break;
+
case NO_THEORY_REGISTRATION:
theoryRegistration = false;
break;
arithPropagation = false;
break;
+ case DISABLE_SYMMETRY_BREAKER:
+ ufSymmetryBreaker = false;
+ break;
+
case RANDOM_SEED:
satRandomSeed = atof(optarg);
break;
/** Should we exit after parsing? */
bool parseOnly;
+ /** Should we exit after preprocessing? */
+ bool preprocessOnly;
+
/** Should the parser do semantic checks? */
bool semanticChecks;
*/
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();
/**
NEQ016_size5_reduced2b.smt \
dead_dnd002.smt \
iso_brn001.smt \
+ gensys_brn001.smt2 \
simple.01.cvc \
simple.02.cvc \
simple.03.cvc \
simple.04.cvc
EXTRA_DIST = $(TESTS) \
- euf_simp09.tim.smt
+ euf_simp09.tim.smt \
+ mkpidgeon
#if CVC4_BUILD_PROFILE_COMPETITION
#else
--- /dev/null
+(set-logic QF_UF)
+(set-info :source |
+http://www.cs.bham.ac.uk/~vxs/quasigroups/benchmark/
+
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-sort U 0)
+(declare-sort I 0)
+(declare-fun unit () I)
+(declare-fun op (I I) I)
+(declare-fun e5 () I)
+(declare-fun e4 () I)
+(declare-fun e3 () I)
+(declare-fun e2 () I)
+(declare-fun e1 () I)
+(declare-fun e0 () I)
+(assert (let ((?v_0 (op e0 e0)) (?v_1 (op e0 e1)) (?v_2 (op e0 e2)) (?v_3 (op e0 e3)) (?v_4 (op e0 e4)) (?v_5 (op e0 e5)) (?v_6 (op e1 e0)) (?v_7 (op e1 e1)) (?v_8 (op e1 e2)) (?v_9 (op e1 e3)) (?v_10 (op e1 e4)) (?v_11 (op e1 e5)) (?v_12 (op e2 e0)) (?v_13 (op e2 e1)) (?v_14 (op e2 e2)) (?v_15 (op e2 e3)) (?v_16 (op e2 e4)) (?v_17 (op e2 e5)) (?v_18 (op e3 e0)) (?v_19 (op e3 e1)) (?v_20 (op e3 e2)) (?v_21 (op e3 e3)) (?v_22 (op e3 e4)) (?v_23 (op e3 e5)) (?v_24 (op e4 e0)) (?v_25 (op e4 e1)) (?v_26 (op e4 e2)) (?v_27 (op e4 e3)) (?v_28 (op e4 e4)) (?v_29 (op e4 e5)) (?v_30 (op e5 e0)) (?v_31 (op e5 e1)) (?v_32 (op e5 e2)) (?v_33 (op e5 e3)) (?v_34 (op e5 e4)) (?v_35 (op e5 e5))) (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (= ?v_0 e0) (= ?v_0 e1)) (= ?v_0 e2)) (= ?v_0 e3)) (= ?v_0 e4)) (= ?v_0 e5)) (or (or (or (or (or (= ?v_1 e0) (= ?v_1 e1)) (= ?v_1 e2)) (= ?v_1 e3)) (= ?v_1 e4)) (= ?v_1 e5))) (or (or (or (or (or (= ?v_2 e0) (= ?v_2 e1)) (= ?v_2 e2)) (= ?v_2 e3)) (= ?v_2 e4)) (= ?v_2 e5))) (or (or (or (or (or (= ?v_3 e0) (= ?v_3 e1)) (= ?v_3 e2)) (= ?v_3 e3)) (= ?v_3 e4)) (= ?v_3 e5))) (or (or (or (or (or (= ?v_4 e0) (= ?v_4 e1)) (= ?v_4 e2)) (= ?v_4 e3)) (= ?v_4 e4)) (= ?v_4 e5))) (or (or (or (or (or (= ?v_5 e0) (= ?v_5 e1)) (= ?v_5 e2)) (= ?v_5 e3)) (= ?v_5 e4)) (= ?v_5 e5))) (and (and (and (and (and (or (or (or (or (or (= ?v_6 e0) (= ?v_6 e1)) (= ?v_6 e2)) (= ?v_6 e3)) (= ?v_6 e4)) (= ?v_6 e5)) (or (or (or (or (or (= ?v_7 e0) (= ?v_7 e1)) (= ?v_7 e2)) (= ?v_7 e3)) (= ?v_7 e4)) (= ?v_7 e5))) (or (or (or (or (or (= ?v_8 e0) (= ?v_8 e1)) (= ?v_8 e2)) (= ?v_8 e3)) (= ?v_8 e4)) (= ?v_8 e5))) (or (or (or (or (or (= ?v_9 e0) (= ?v_9 e1)) (= ?v_9 e2)) (= ?v_9 e3)) (= ?v_9 e4)) (= ?v_9 e5))) (or (or (or (or (or (= ?v_10 e0) (= ?v_10 e1)) (= ?v_10 e2)) (= ?v_10 e3)) (= ?v_10 e4)) (= ?v_10 e5))) (or (or (or (or (or (= ?v_11 e0) (= ?v_11 e1)) (= ?v_11 e2)) (= ?v_11 e3)) (= ?v_11 e4)) (= ?v_11 e5)))) (and (and (and (and (and (or (or (or (or (or (= ?v_12 e0) (= ?v_12 e1)) (= ?v_12 e2)) (= ?v_12 e3)) (= ?v_12 e4)) (= ?v_12 e5)) (or (or (or (or (or (= ?v_13 e0) (= ?v_13 e1)) (= ?v_13 e2)) (= ?v_13 e3)) (= ?v_13 e4)) (= ?v_13 e5))) (or (or (or (or (or (= ?v_14 e0) (= ?v_14 e1)) (= ?v_14 e2)) (= ?v_14 e3)) (= ?v_14 e4)) (= ?v_14 e5))) (or (or (or (or (or (= ?v_15 e0) (= ?v_15 e1)) (= ?v_15 e2)) (= ?v_15 e3)) (= ?v_15 e4)) (= ?v_15 e5))) (or (or (or (or (or (= ?v_16 e0) (= ?v_16 e1)) (= ?v_16 e2)) (= ?v_16 e3)) (= ?v_16 e4)) (= ?v_16 e5))) (or (or (or (or (or (= ?v_17 e0) (= ?v_17 e1)) (= ?v_17 e2)) (= ?v_17 e3)) (= ?v_17 e4)) (= ?v_17 e5)))) (and (and (and (and (and (or (or (or (or (or (= ?v_18 e0) (= ?v_18 e1)) (= ?v_18 e2)) (= ?v_18 e3)) (= ?v_18 e4)) (= ?v_18 e5)) (or (or (or (or (or (= ?v_19 e0) (= ?v_19 e1)) (= ?v_19 e2)) (= ?v_19 e3)) (= ?v_19 e4)) (= ?v_19 e5))) (or (or (or (or (or (= ?v_20 e0) (= ?v_20 e1)) (= ?v_20 e2)) (= ?v_20 e3)) (= ?v_20 e4)) (= ?v_20 e5))) (or (or (or (or (or (= ?v_21 e0) (= ?v_21 e1)) (= ?v_21 e2)) (= ?v_21 e3)) (= ?v_21 e4)) (= ?v_21 e5))) (or (or (or (or (or (= ?v_22 e0) (= ?v_22 e1)) (= ?v_22 e2)) (= ?v_22 e3)) (= ?v_22 e4)) (= ?v_22 e5))) (or (or (or (or (or (= ?v_23 e0) (= ?v_23 e1)) (= ?v_23 e2)) (= ?v_23 e3)) (= ?v_23 e4)) (= ?v_23 e5)))) (and (and (and (and (and (or (or (or (or (or (= ?v_24 e0) (= ?v_24 e1)) (= ?v_24 e2)) (= ?v_24 e3)) (= ?v_24 e4)) (= ?v_24 e5)) (or (or (or (or (or (= ?v_25 e0) (= ?v_25 e1)) (= ?v_25 e2)) (= ?v_25 e3)) (= ?v_25 e4)) (= ?v_25 e5))) (or (or (or (or (or (= ?v_26 e0) (= ?v_26 e1)) (= ?v_26 e2)) (= ?v_26 e3)) (= ?v_26 e4)) (= ?v_26 e5))) (or (or (or (or (or (= ?v_27 e0) (= ?v_27 e1)) (= ?v_27 e2)) (= ?v_27 e3)) (= ?v_27 e4)) (= ?v_27 e5))) (or (or (or (or (or (= ?v_28 e0) (= ?v_28 e1)) (= ?v_28 e2)) (= ?v_28 e3)) (= ?v_28 e4)) (= ?v_28 e5))) (or (or (or (or (or (= ?v_29 e0) (= ?v_29 e1)) (= ?v_29 e2)) (= ?v_29 e3)) (= ?v_29 e4)) (= ?v_29 e5)))) (and (and (and (and (and (or (or (or (or (or (= ?v_30 e0) (= ?v_30 e1)) (= ?v_30 e2)) (= ?v_30 e3)) (= ?v_30 e4)) (= ?v_30 e5)) (or (or (or (or (or (= ?v_31 e0) (= ?v_31 e1)) (= ?v_31 e2)) (= ?v_31 e3)) (= ?v_31 e4)) (= ?v_31 e5))) (or (or (or (or (or (= ?v_32 e0) (= ?v_32 e1)) (= ?v_32 e2)) (= ?v_32 e3)) (= ?v_32 e4)) (= ?v_32 e5))) (or (or (or (or (or (= ?v_33 e0) (= ?v_33 e1)) (= ?v_33 e2)) (= ?v_33 e3)) (= ?v_33 e4)) (= ?v_33 e5))) (or (or (or (or (or (= ?v_34 e0) (= ?v_34 e1)) (= ?v_34 e2)) (= ?v_34 e3)) (= ?v_34 e4)) (= ?v_34 e5))) (or (or (or (or (or (= ?v_35 e0) (= ?v_35 e1)) (= ?v_35 e2)) (= ?v_35 e3)) (= ?v_35 e4)) (= ?v_35 e5))))))
+(assert (let ((?v_1 (op e0 e0)) (?v_2 (op e0 e1)) (?v_3 (op e0 e2)) (?v_4 (op e0 e3)) (?v_5 (op e0 e4)) (?v_6 (op e0 e5)) (?v_8 (op e1 e0)) (?v_21 (op e1 e1)) (?v_22 (op e1 e2)) (?v_23 (op e1 e3)) (?v_24 (op e1 e4)) (?v_25 (op e1 e5)) (?v_9 (op e2 e0)) (?v_28 (op e2 e1)) (?v_51 (op e2 e2)) (?v_52 (op e2 e3)) (?v_53 (op e2 e4)) (?v_54 (op e2 e5)) (?v_10 (op e3 e0)) (?v_29 (op e3 e1)) (?v_58 (op e3 e2)) (?v_91 (op e3 e3)) (?v_92 (op e3 e4)) (?v_93 (op e3 e5)) (?v_11 (op e4 e0)) (?v_30 (op e4 e1)) (?v_59 (op e4 e2)) (?v_98 (op e4 e3)) (?v_141 (op e4 e4)) (?v_142 (op e4 e5)) (?v_12 (op e5 e0)) (?v_31 (op e5 e1)) (?v_60 (op e5 e2)) (?v_99 (op e5 e3)) (?v_148 (op e5 e4)) (?v_201 (op e5 e5))) (let ((?v_0 (= ?v_1 e0)) (?v_7 (= ?v_1 e1)) (?v_13 (= ?v_1 e2)) (?v_14 (= ?v_1 e3)) (?v_15 (= ?v_1 e4)) (?v_16 (= ?v_1 e5)) (?v_18 (= ?v_2 e0)) (?v_26 (= ?v_2 e1)) (?v_33 (= ?v_2 e2)) (?v_36 (= ?v_2 e3)) (?v_39 (= ?v_2 e4)) (?v_42 (= ?v_2 e5)) (?v_46 (= ?v_3 e0)) (?v_55 (= ?v_3 e1)) (?v_63 (= ?v_3 e2)) (?v_68 (= ?v_3 e3)) (?v_73 (= ?v_3 e4)) (?v_78 (= ?v_3 e5)) (?v_84 (= ?v_4 e0)) (?v_94 (= ?v_4 e1)) (?v_103 (= ?v_4 e2)) (?v_110 (= ?v_4 e3)) (?v_117 (= ?v_4 e4)) (?v_124 (= ?v_4 e5)) (?v_132 (= ?v_5 e0)) (?v_143 (= ?v_5 e1)) (?v_153 (= ?v_5 e2)) (?v_162 (= ?v_5 e3)) (?v_171 (= ?v_5 e4)) (?v_180 (= ?v_5 e5)) (?v_190 (= ?v_6 e0)) (?v_202 (= ?v_6 e1)) (?v_213 (= ?v_6 e2)) (?v_224 (= ?v_6 e3)) (?v_235 (= ?v_6 e4)) (?v_246 (= ?v_6 e5)) (?v_17 (= ?v_8 e0)) (?v_20 (= ?v_8 e1)) (?v_32 (= ?v_8 e2)) (?v_35 (= ?v_8 e3)) (?v_38 (= ?v_8 e4)) (?v_41 (= ?v_8 e5)) (?v_19 (= ?v_21 e0)) (?v_27 (= ?v_21 e1)) (?v_34 (= ?v_21 e2)) (?v_37 (= ?v_21 e3)) (?v_40 (= ?v_21 e4)) (?v_43 (= ?v_21 e5)) (?v_47 (= ?v_22 e0)) (?v_56 (= ?v_22 e1)) (?v_64 (= ?v_22 e2)) (?v_69 (= ?v_22 e3)) (?v_74 (= ?v_22 e4)) (?v_79 (= ?v_22 e5)) (?v_85 (= ?v_23 e0)) (?v_95 (= ?v_23 e1)) (?v_104 (= ?v_23 e2)) (?v_111 (= ?v_23 e3)) (?v_118 (= ?v_23 e4)) (?v_125 (= ?v_23 e5)) (?v_133 (= ?v_24 e0)) (?v_144 (= ?v_24 e1)) (?v_154 (= ?v_24 e2)) (?v_163 (= ?v_24 e3)) (?v_172 (= ?v_24 e4)) (?v_181 (= ?v_24 e5)) (?v_191 (= ?v_25 e0)) (?v_203 (= ?v_25 e1)) (?v_214 (= ?v_25 e2)) (?v_225 (= ?v_25 e3)) (?v_236 (= ?v_25 e4)) (?v_247 (= ?v_25 e5)) (?v_44 (= ?v_9 e0)) (?v_49 (= ?v_9 e1)) (?v_61 (= ?v_9 e2)) (?v_66 (= ?v_9 e3)) (?v_71 (= ?v_9 e4)) (?v_76 (= ?v_9 e5)) (?v_45 (= ?v_28 e0)) (?v_50 (= ?v_28 e1)) (?v_62 (= ?v_28 e2)) (?v_67 (= ?v_28 e3)) (?v_72 (= ?v_28 e4)) (?v_77 (= ?v_28 e5)) (?v_48 (= ?v_51 e0)) (?v_57 (= ?v_51 e1)) (?v_65 (= ?v_51 e2)) (?v_70 (= ?v_51 e3)) (?v_75 (= ?v_51 e4)) (?v_80 (= ?v_51 e5)) (?v_86 (= ?v_52 e0)) (?v_96 (= ?v_52 e1)) (?v_105 (= ?v_52 e2)) (?v_112 (= ?v_52 e3)) (?v_119 (= ?v_52 e4)) (?v_126 (= ?v_52 e5)) (?v_134 (= ?v_53 e0)) (?v_145 (= ?v_53 e1)) (?v_155 (= ?v_53 e2)) (?v_164 (= ?v_53 e3)) (?v_173 (= ?v_53 e4)) (?v_182 (= ?v_53 e5)) (?v_192 (= ?v_54 e0)) (?v_204 (= ?v_54 e1)) (?v_215 (= ?v_54 e2)) (?v_226 (= ?v_54 e3)) (?v_237 (= ?v_54 e4)) (?v_248 (= ?v_54 e5)) (?v_81 (= ?v_10 e0)) (?v_88 (= ?v_10 e1)) (?v_100 (= ?v_10 e2)) (?v_107 (= ?v_10 e3)) (?v_114 (= ?v_10 e4)) (?v_121 (= ?v_10 e5)) (?v_82 (= ?v_29 e0)) (?v_89 (= ?v_29 e1)) (?v_101 (= ?v_29 e2)) (?v_108 (= ?v_29 e3)) (?v_115 (= ?v_29 e4)) (?v_122 (= ?v_29 e5)) (?v_83 (= ?v_58 e0)) (?v_90 (= ?v_58 e1)) (?v_102 (= ?v_58 e2)) (?v_109 (= ?v_58 e3)) (?v_116 (= ?v_58 e4)) (?v_123 (= ?v_58 e5)) (?v_87 (= ?v_91 e0)) (?v_97 (= ?v_91 e1)) (?v_106 (= ?v_91 e2)) (?v_113 (= ?v_91 e3)) (?v_120 (= ?v_91 e4)) (?v_127 (= ?v_91 e5)) (?v_135 (= ?v_92 e0)) (?v_146 (= ?v_92 e1)) (?v_156 (= ?v_92 e2)) (?v_165 (= ?v_92 e3)) (?v_174 (= ?v_92 e4)) (?v_183 (= ?v_92 e5)) (?v_193 (= ?v_93 e0)) (?v_205 (= ?v_93 e1)) (?v_216 (= ?v_93 e2)) (?v_227 (= ?v_93 e3)) (?v_238 (= ?v_93 e4)) (?v_249 (= ?v_93 e5)) (?v_128 (= ?v_11 e0)) (?v_137 (= ?v_11 e1)) (?v_149 (= ?v_11 e2)) (?v_158 (= ?v_11 e3)) (?v_167 (= ?v_11 e4)) (?v_176 (= ?v_11 e5)) (?v_129 (= ?v_30 e0)) (?v_138 (= ?v_30 e1)) (?v_150 (= ?v_30 e2)) (?v_159 (= ?v_30 e3)) (?v_168 (= ?v_30 e4)) (?v_177 (= ?v_30 e5)) (?v_130 (= ?v_59 e0)) (?v_139 (= ?v_59 e1)) (?v_151 (= ?v_59 e2)) (?v_160 (= ?v_59 e3)) (?v_169 (= ?v_59 e4)) (?v_178 (= ?v_59 e5)) (?v_131 (= ?v_98 e0)) (?v_140 (= ?v_98 e1)) (?v_152 (= ?v_98 e2)) (?v_161 (= ?v_98 e3)) (?v_170 (= ?v_98 e4)) (?v_179 (= ?v_98 e5)) (?v_136 (= ?v_141 e0)) (?v_147 (= ?v_141 e1)) (?v_157 (= ?v_141 e2)) (?v_166 (= ?v_141 e3)) (?v_175 (= ?v_141 e4)) (?v_184 (= ?v_141 e5)) (?v_194 (= ?v_142 e0)) (?v_206 (= ?v_142 e1)) (?v_217 (= ?v_142 e2)) (?v_228 (= ?v_142 e3)) (?v_239 (= ?v_142 e4)) (?v_250 (= ?v_142 e5)) (?v_185 (= ?v_12 e0)) (?v_196 (= ?v_12 e1)) (?v_208 (= ?v_12 e2)) (?v_219 (= ?v_12 e3)) (?v_230 (= ?v_12 e4)) (?v_241 (= ?v_12 e5)) (?v_186 (= ?v_31 e0)) (?v_197 (= ?v_31 e1)) (?v_209 (= ?v_31 e2)) (?v_220 (= ?v_31 e3)) (?v_231 (= ?v_31 e4)) (?v_242 (= ?v_31 e5)) (?v_187 (= ?v_60 e0)) (?v_198 (= ?v_60 e1)) (?v_210 (= ?v_60 e2)) (?v_221 (= ?v_60 e3)) (?v_232 (= ?v_60 e4)) (?v_243 (= ?v_60 e5)) (?v_188 (= ?v_99 e0)) (?v_199 (= ?v_99 e1)) (?v_211 (= ?v_99 e2)) (?v_222 (= ?v_99 e3)) (?v_233 (= ?v_99 e4)) (?v_244 (= ?v_99 e5)) (?v_189 (= ?v_148 e0)) (?v_200 (= ?v_148 e1)) (?v_212 (= ?v_148 e2)) (?v_223 (= ?v_148 e3)) (?v_234 (= ?v_148 e4)) (?v_245 (= ?v_148 e5)) (?v_195 (= ?v_201 e0)) (?v_207 (= ?v_201 e1)) (?v_218 (= ?v_201 e2)) (?v_229 (= ?v_201 e3)) (?v_240 (= ?v_201 e4)) (?v_251 (= ?v_201 e5))) (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or ?v_0 ?v_18) ?v_46) ?v_84) ?v_132) ?v_190) (or (or (or (or (or ?v_0 ?v_17) ?v_44) ?v_81) ?v_128) ?v_185)) (and (or (or (or (or (or ?v_7 ?v_26) ?v_55) ?v_94) ?v_143) ?v_202) (or (or (or (or (or ?v_7 ?v_20) ?v_49) ?v_88) ?v_137) ?v_196))) (and (or (or (or (or (or ?v_13 ?v_33) ?v_63) ?v_103) ?v_153) ?v_213) (or (or (or (or (or ?v_13 ?v_32) ?v_61) ?v_100) ?v_149) ?v_208))) (and (or (or (or (or (or ?v_14 ?v_36) ?v_68) ?v_110) ?v_162) ?v_224) (or (or (or (or (or ?v_14 ?v_35) ?v_66) ?v_107) ?v_158) ?v_219))) (and (or (or (or (or (or ?v_15 ?v_39) ?v_73) ?v_117) ?v_171) ?v_235) (or (or (or (or (or ?v_15 ?v_38) ?v_71) ?v_114) ?v_167) ?v_230))) (and (or (or (or (or (or ?v_16 ?v_42) ?v_78) ?v_124) ?v_180) ?v_246) (or (or (or (or (or ?v_16 ?v_41) ?v_76) ?v_121) ?v_176) ?v_241))) (and (and (and (and (and (and (or (or (or (or (or ?v_17 ?v_19) ?v_47) ?v_85) ?v_133) ?v_191) (or (or (or (or (or ?v_18 ?v_19) ?v_45) ?v_82) ?v_129) ?v_186)) (and (or (or (or (or (or ?v_20 ?v_27) ?v_56) ?v_95) ?v_144) ?v_203) (or (or (or (or (or ?v_26 ?v_27) ?v_50) ?v_89) ?v_138) ?v_197))) (and (or (or (or (or (or ?v_32 ?v_34) ?v_64) ?v_104) ?v_154) ?v_214) (or (or (or (or (or ?v_33 ?v_34) ?v_62) ?v_101) ?v_150) ?v_209))) (and (or (or (or (or (or ?v_35 ?v_37) ?v_69) ?v_111) ?v_163) ?v_225) (or (or (or (or (or ?v_36 ?v_37) ?v_67) ?v_108) ?v_159) ?v_220))) (and (or (or (or (or (or ?v_38 ?v_40) ?v_74) ?v_118) ?v_172) ?v_236) (or (or (or (or (or ?v_39 ?v_40) ?v_72) ?v_115) ?v_168) ?v_231))) (and (or (or (or (or (or ?v_41 ?v_43) ?v_79) ?v_125) ?v_181) ?v_247) (or (or (or (or (or ?v_42 ?v_43) ?v_77) ?v_122) ?v_177) ?v_242)))) (and (and (and (and (and (and (or (or (or (or (or ?v_44 ?v_45) ?v_48) ?v_86) ?v_134) ?v_192) (or (or (or (or (or ?v_46 ?v_47) ?v_48) ?v_83) ?v_130) ?v_187)) (and (or (or (or (or (or ?v_49 ?v_50) ?v_57) ?v_96) ?v_145) ?v_204) (or (or (or (or (or ?v_55 ?v_56) ?v_57) ?v_90) ?v_139) ?v_198))) (and (or (or (or (or (or ?v_61 ?v_62) ?v_65) ?v_105) ?v_155) ?v_215) (or (or (or (or (or ?v_63 ?v_64) ?v_65) ?v_102) ?v_151) ?v_210))) (and (or (or (or (or (or ?v_66 ?v_67) ?v_70) ?v_112) ?v_164) ?v_226) (or (or (or (or (or ?v_68 ?v_69) ?v_70) ?v_109) ?v_160) ?v_221))) (and (or (or (or (or (or ?v_71 ?v_72) ?v_75) ?v_119) ?v_173) ?v_237) (or (or (or (or (or ?v_73 ?v_74) ?v_75) ?v_116) ?v_169) ?v_232))) (and (or (or (or (or (or ?v_76 ?v_77) ?v_80) ?v_126) ?v_182) ?v_248) (or (or (or (or (or ?v_78 ?v_79) ?v_80) ?v_123) ?v_178) ?v_243)))) (and (and (and (and (and (and (or (or (or (or (or ?v_81 ?v_82) ?v_83) ?v_87) ?v_135) ?v_193) (or (or (or (or (or ?v_84 ?v_85) ?v_86) ?v_87) ?v_131) ?v_188)) (and (or (or (or (or (or ?v_88 ?v_89) ?v_90) ?v_97) ?v_146) ?v_205) (or (or (or (or (or ?v_94 ?v_95) ?v_96) ?v_97) ?v_140) ?v_199))) (and (or (or (or (or (or ?v_100 ?v_101) ?v_102) ?v_106) ?v_156) ?v_216) (or (or (or (or (or ?v_103 ?v_104) ?v_105) ?v_106) ?v_152) ?v_211))) (and (or (or (or (or (or ?v_107 ?v_108) ?v_109) ?v_113) ?v_165) ?v_227) (or (or (or (or (or ?v_110 ?v_111) ?v_112) ?v_113) ?v_161) ?v_222))) (and (or (or (or (or (or ?v_114 ?v_115) ?v_116) ?v_120) ?v_174) ?v_238) (or (or (or (or (or ?v_117 ?v_118) ?v_119) ?v_120) ?v_170) ?v_233))) (and (or (or (or (or (or ?v_121 ?v_122) ?v_123) ?v_127) ?v_183) ?v_249) (or (or (or (or (or ?v_124 ?v_125) ?v_126) ?v_127) ?v_179) ?v_244)))) (and (and (and (and (and (and (or (or (or (or (or ?v_128 ?v_129) ?v_130) ?v_131) ?v_136) ?v_194) (or (or (or (or (or ?v_132 ?v_133) ?v_134) ?v_135) ?v_136) ?v_189)) (and (or (or (or (or (or ?v_137 ?v_138) ?v_139) ?v_140) ?v_147) ?v_206) (or (or (or (or (or ?v_143 ?v_144) ?v_145) ?v_146) ?v_147) ?v_200))) (and (or (or (or (or (or ?v_149 ?v_150) ?v_151) ?v_152) ?v_157) ?v_217) (or (or (or (or (or ?v_153 ?v_154) ?v_155) ?v_156) ?v_157) ?v_212))) (and (or (or (or (or (or ?v_158 ?v_159) ?v_160) ?v_161) ?v_166) ?v_228) (or (or (or (or (or ?v_162 ?v_163) ?v_164) ?v_165) ?v_166) ?v_223))) (and (or (or (or (or (or ?v_167 ?v_168) ?v_169) ?v_170) ?v_175) ?v_239) (or (or (or (or (or ?v_171 ?v_172) ?v_173) ?v_174) ?v_175) ?v_234))) (and (or (or (or (or (or ?v_176 ?v_177) ?v_178) ?v_179) ?v_184) ?v_250) (or (or (or (or (or ?v_180 ?v_181) ?v_182) ?v_183) ?v_184) ?v_245)))) (and (and (and (and (and (and (or (or (or (or (or ?v_185 ?v_186) ?v_187) ?v_188) ?v_189) ?v_195) (or (or (or (or (or ?v_190 ?v_191) ?v_192) ?v_193) ?v_194) ?v_195)) (and (or (or (or (or (or ?v_196 ?v_197) ?v_198) ?v_199) ?v_200) ?v_207) (or (or (or (or (or ?v_202 ?v_203) ?v_204) ?v_205) ?v_206) ?v_207))) (and (or (or (or (or (or ?v_208 ?v_209) ?v_210) ?v_211) ?v_212) ?v_218) (or (or (or (or (or ?v_213 ?v_214) ?v_215) ?v_216) ?v_217) ?v_218))) (and (or (or (or (or (or ?v_219 ?v_220) ?v_221) ?v_222) ?v_223) ?v_229) (or (or (or (or (or ?v_224 ?v_225) ?v_226) ?v_227) ?v_228) ?v_229))) (and (or (or (or (or (or ?v_230 ?v_231) ?v_232) ?v_233) ?v_234) ?v_240) (or (or (or (or (or ?v_235 ?v_236) ?v_237) ?v_238) ?v_239) ?v_240))) (and (or (or (or (or (or ?v_241 ?v_242) ?v_243) ?v_244) ?v_245) ?v_251) (or (or (or (or (or ?v_246 ?v_247) ?v_248) ?v_249) ?v_250) ?v_251)))))))
+(assert (and (and (and (and (and (and (and (= (op unit e0) e0) (= (op e0 unit) e0)) (and (= (op unit e1) e1) (= (op e1 unit) e1))) (and (= (op unit e2) e2) (= (op e2 unit) e2))) (and (= (op unit e3) e3) (= (op e3 unit) e3))) (and (= (op unit e4) e4) (= (op e4 unit) e4))) (and (= (op unit e5) e5) (= (op e5 unit) e5))) (or (or (or (or (or (= unit e0) (= unit e1)) (= unit e2)) (= unit e3)) (= unit e4)) (= unit e5))))
+(assert (= unit e0))
+(assert (let ((?v_0 (op e0 e0)) (?v_6 (op e0 e1)) (?v_12 (op e0 e2)) (?v_18 (op e0 e3)) (?v_24 (op e0 e4)) (?v_30 (op e0 e5)) (?v_1 (op e1 e0)) (?v_7 (op e1 e1)) (?v_13 (op e1 e2)) (?v_19 (op e1 e3)) (?v_25 (op e1 e4)) (?v_31 (op e1 e5)) (?v_2 (op e2 e0)) (?v_8 (op e2 e1)) (?v_14 (op e2 e2)) (?v_20 (op e2 e3)) (?v_26 (op e2 e4)) (?v_32 (op e2 e5)) (?v_3 (op e3 e0)) (?v_9 (op e3 e1)) (?v_15 (op e3 e2)) (?v_21 (op e3 e3)) (?v_27 (op e3 e4)) (?v_33 (op e3 e5)) (?v_4 (op e4 e0)) (?v_10 (op e4 e1)) (?v_16 (op e4 e2)) (?v_22 (op e4 e3)) (?v_28 (op e4 e4)) (?v_34 (op e4 e5)) (?v_5 (op e5 e0)) (?v_11 (op e5 e1)) (?v_17 (op e5 e2)) (?v_23 (op e5 e3)) (?v_29 (op e5 e4)) (?v_35 (op e5 e5))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_0 ?v_1)) (not (= ?v_0 ?v_2))) (not (= ?v_0 ?v_3))) (not (= ?v_0 ?v_4))) (not (= ?v_0 ?v_5))) (not (= ?v_1 ?v_2))) (not (= ?v_1 ?v_3))) (not (= ?v_1 ?v_4))) (not (= ?v_1 ?v_5))) (not (= ?v_2 ?v_3))) (not (= ?v_2 ?v_4))) (not (= ?v_2 ?v_5))) (not (= ?v_3 ?v_4))) (not (= ?v_3 ?v_5))) (not (= ?v_4 ?v_5))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_6 ?v_7)) (not (= ?v_6 ?v_8))) (not (= ?v_6 ?v_9))) (not (= ?v_6 ?v_10))) (not (= ?v_6 ?v_11))) (not (= ?v_7 ?v_8))) (not (= ?v_7 ?v_9))) (not (= ?v_7 ?v_10))) (not (= ?v_7 ?v_11))) (not (= ?v_8 ?v_9))) (not (= ?v_8 ?v_10))) (not (= ?v_8 ?v_11))) (not (= ?v_9 ?v_10))) (not (= ?v_9 ?v_11))) (not (= ?v_10 ?v_11)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_12 ?v_13)) (not (= ?v_12 ?v_14))) (not (= ?v_12 ?v_15))) (not (= ?v_12 ?v_16))) (not (= ?v_12 ?v_17))) (not (= ?v_13 ?v_14))) (not (= ?v_13 ?v_15))) (not (= ?v_13 ?v_16))) (not (= ?v_13 ?v_17))) (not (= ?v_14 ?v_15))) (not (= ?v_14 ?v_16))) (not (= ?v_14 ?v_17))) (not (= ?v_15 ?v_16))) (not (= ?v_15 ?v_17))) (not (= ?v_16 ?v_17)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_18 ?v_19)) (not (= ?v_18 ?v_20))) (not (= ?v_18 ?v_21))) (not (= ?v_18 ?v_22))) (not (= ?v_18 ?v_23))) (not (= ?v_19 ?v_20))) (not (= ?v_19 ?v_21))) (not (= ?v_19 ?v_22))) (not (= ?v_19 ?v_23))) (not (= ?v_20 ?v_21))) (not (= ?v_20 ?v_22))) (not (= ?v_20 ?v_23))) (not (= ?v_21 ?v_22))) (not (= ?v_21 ?v_23))) (not (= ?v_22 ?v_23)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_24 ?v_25)) (not (= ?v_24 ?v_26))) (not (= ?v_24 ?v_27))) (not (= ?v_24 ?v_28))) (not (= ?v_24 ?v_29))) (not (= ?v_25 ?v_26))) (not (= ?v_25 ?v_27))) (not (= ?v_25 ?v_28))) (not (= ?v_25 ?v_29))) (not (= ?v_26 ?v_27))) (not (= ?v_26 ?v_28))) (not (= ?v_26 ?v_29))) (not (= ?v_27 ?v_28))) (not (= ?v_27 ?v_29))) (not (= ?v_28 ?v_29)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_30 ?v_31)) (not (= ?v_30 ?v_32))) (not (= ?v_30 ?v_33))) (not (= ?v_30 ?v_34))) (not (= ?v_30 ?v_35))) (not (= ?v_31 ?v_32))) (not (= ?v_31 ?v_33))) (not (= ?v_31 ?v_34))) (not (= ?v_31 ?v_35))) (not (= ?v_32 ?v_33))) (not (= ?v_32 ?v_34))) (not (= ?v_32 ?v_35))) (not (= ?v_33 ?v_34))) (not (= ?v_33 ?v_35))) (not (= ?v_34 ?v_35)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_0 ?v_6)) (not (= ?v_0 ?v_12))) (not (= ?v_0 ?v_18))) (not (= ?v_0 ?v_24))) (not (= ?v_0 ?v_30))) (not (= ?v_6 ?v_12))) (not (= ?v_6 ?v_18))) (not (= ?v_6 ?v_24))) (not (= ?v_6 ?v_30))) (not (= ?v_12 ?v_18))) (not (= ?v_12 ?v_24))) (not (= ?v_12 ?v_30))) (not (= ?v_18 ?v_24))) (not (= ?v_18 ?v_30))) (not (= ?v_24 ?v_30))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_1 ?v_7)) (not (= ?v_1 ?v_13))) (not (= ?v_1 ?v_19))) (not (= ?v_1 ?v_25))) (not (= ?v_1 ?v_31))) (not (= ?v_7 ?v_13))) (not (= ?v_7 ?v_19))) (not (= ?v_7 ?v_25))) (not (= ?v_7 ?v_31))) (not (= ?v_13 ?v_19))) (not (= ?v_13 ?v_25))) (not (= ?v_13 ?v_31))) (not (= ?v_19 ?v_25))) (not (= ?v_19 ?v_31))) (not (= ?v_25 ?v_31)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_2 ?v_8)) (not (= ?v_2 ?v_14))) (not (= ?v_2 ?v_20))) (not (= ?v_2 ?v_26))) (not (= ?v_2 ?v_32))) (not (= ?v_8 ?v_14))) (not (= ?v_8 ?v_20))) (not (= ?v_8 ?v_26))) (not (= ?v_8 ?v_32))) (not (= ?v_14 ?v_20))) (not (= ?v_14 ?v_26))) (not (= ?v_14 ?v_32))) (not (= ?v_20 ?v_26))) (not (= ?v_20 ?v_32))) (not (= ?v_26 ?v_32)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_3 ?v_9)) (not (= ?v_3 ?v_15))) (not (= ?v_3 ?v_21))) (not (= ?v_3 ?v_27))) (not (= ?v_3 ?v_33))) (not (= ?v_9 ?v_15))) (not (= ?v_9 ?v_21))) (not (= ?v_9 ?v_27))) (not (= ?v_9 ?v_33))) (not (= ?v_15 ?v_21))) (not (= ?v_15 ?v_27))) (not (= ?v_15 ?v_33))) (not (= ?v_21 ?v_27))) (not (= ?v_21 ?v_33))) (not (= ?v_27 ?v_33)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_4 ?v_10)) (not (= ?v_4 ?v_16))) (not (= ?v_4 ?v_22))) (not (= ?v_4 ?v_28))) (not (= ?v_4 ?v_34))) (not (= ?v_10 ?v_16))) (not (= ?v_10 ?v_22))) (not (= ?v_10 ?v_28))) (not (= ?v_10 ?v_34))) (not (= ?v_16 ?v_22))) (not (= ?v_16 ?v_28))) (not (= ?v_16 ?v_34))) (not (= ?v_22 ?v_28))) (not (= ?v_22 ?v_34))) (not (= ?v_28 ?v_34)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_5 ?v_11)) (not (= ?v_5 ?v_17))) (not (= ?v_5 ?v_23))) (not (= ?v_5 ?v_29))) (not (= ?v_5 ?v_35))) (not (= ?v_11 ?v_17))) (not (= ?v_11 ?v_23))) (not (= ?v_11 ?v_29))) (not (= ?v_11 ?v_35))) (not (= ?v_17 ?v_23))) (not (= ?v_17 ?v_29))) (not (= ?v_17 ?v_35))) (not (= ?v_23 ?v_29))) (not (= ?v_23 ?v_35))) (not (= ?v_29 ?v_35)))))))
+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= e0 e1)) (not (= e0 e2))) (not (= e0 e3))) (not (= e0 e4))) (not (= e0 e5))) (not (= e1 e2))) (not (= e1 e3))) (not (= e1 e4))) (not (= e1 e5))) (not (= e2 e3))) (not (= e2 e4))) (not (= e2 e5))) (not (= e3 e4))) (not (= e3 e5))) (not (= e4 e5))))
+(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e2 (op e1 e1))) (= e3 (op e4 e4))) (= e4 (op e5 e2))) (= e5 (op e2 e1)))))
+(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e2 (op e1 e1))) (= e3 (op e5 e5))) (= e5 (op e4 e2))) (= e4 (op e2 e1)))))
+(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e2 (op e1 e1))) (= e4 (op e3 e3))) (= e3 (op e5 e2))) (= e5 (op e2 e1)))))
+(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e2 (op e1 e1))) (= e4 (op e5 e5))) (= e5 (op e3 e2))) (= e3 (op e2 e1)))))
+(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e2 (op e1 e1))) (= e5 (op e3 e3))) (= e3 (op e4 e2))) (= e4 (op e2 e1)))))
+(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e2 (op e1 e1))) (= e5 (op e4 e4))) (= e4 (op e3 e2))) (= e3 (op e2 e1)))))
+(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e3 (op e1 e1))) (= e2 (op e4 e4))) (= e4 (op e5 e3))) (= e5 (op e3 e1)))))
+(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e3 (op e1 e1))) (= e2 (op e5 e5))) (= e5 (op e4 e3))) (= e4 (op e3 e1)))))
+(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e3 (op e1 e1))) (= e4 (op e2 e2))) (= e2 (op e5 e3))) (= e5 (op e3 e1)))))
+(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e3 (op e1 e1))) (= e4 (op e5 e5))) (= e5 (op e2 e3))) (= e2 (op e3 e1)))))
+(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e3 (op e1 e1))) (= e5 (op e2 e2))) (= e2 (op e4 e3))) (= e4 (op e3 e1)))))
+(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e3 (op e1 e1))) (= e5 (op e4 e4))) (= e4 (op e2 e3))) (= e2 (op e3 e1)))))
+(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e4 (op e1 e1))) (= e2 (op e3 e3))) (= e3 (op e5 e4))) (= e5 (op e4 e1)))))
+(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e4 (op e1 e1))) (= e2 (op e5 e5))) (= e5 (op e3 e4))) (= e3 (op e4 e1)))))
+(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e4 (op e1 e1))) (= e3 (op e2 e2))) (= e2 (op e5 e4))) (= e5 (op e4 e1)))))
+(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e4 (op e1 e1))) (= e3 (op e5 e5))) (= e5 (op e2 e4))) (= e2 (op e4 e1)))))
+(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e4 (op e1 e1))) (= e5 (op e2 e2))) (= e2 (op e3 e4))) (= e3 (op e4 e1)))))
+(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e4 (op e1 e1))) (= e5 (op e3 e3))) (= e3 (op e2 e4))) (= e2 (op e4 e1)))))
+(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e5 (op e1 e1))) (= e2 (op e3 e3))) (= e3 (op e4 e5))) (= e4 (op e5 e1)))))
+(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e5 (op e1 e1))) (= e2 (op e4 e4))) (= e4 (op e3 e5))) (= e3 (op e5 e1)))))
+(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e5 (op e1 e1))) (= e3 (op e2 e2))) (= e2 (op e4 e5))) (= e4 (op e5 e1)))))
+(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e5 (op e1 e1))) (= e3 (op e4 e4))) (= e4 (op e2 e5))) (= e2 (op e5 e1)))))
+(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e5 (op e1 e1))) (= e4 (op e2 e2))) (= e2 (op e3 e5))) (= e3 (op e5 e1)))))
+(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e5 (op e1 e1))) (= e4 (op e3 e3))) (= e3 (op e2 e5))) (= e2 (op e5 e1)))))
+(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e1 (op e2 e2))) (= e3 (op e4 e4))) (= e4 (op e5 e1))) (= e5 (op e1 e2)))))
+(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e1 (op e2 e2))) (= e3 (op e5 e5))) (= e5 (op e4 e1))) (= e4 (op e1 e2)))))
+(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e1 (op e2 e2))) (= e4 (op e3 e3))) (= e3 (op e5 e1))) (= e5 (op e1 e2)))))
+(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e1 (op e2 e2))) (= e4 (op e5 e5))) (= e5 (op e3 e1))) (= e3 (op e1 e2)))))
+(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e1 (op e2 e2))) (= e5 (op e3 e3))) (= e3 (op e4 e1))) (= e4 (op e1 e2)))))
+(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e1 (op e2 e2))) (= e5 (op e4 e4))) (= e4 (op e3 e1))) (= e3 (op e1 e2)))))
+(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e3 (op e2 e2))) (= e1 (op e4 e4))) (= e4 (op e5 e3))) (= e5 (op e3 e2)))))
+(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e3 (op e2 e2))) (= e1 (op e5 e5))) (= e5 (op e4 e3))) (= e4 (op e3 e2)))))
+(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e3 (op e2 e2))) (= e4 (op e1 e1))) (= e1 (op e5 e3))) (= e5 (op e3 e2)))))
+(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e3 (op e2 e2))) (= e4 (op e5 e5))) (= e5 (op e1 e3))) (= e1 (op e3 e2)))))
+(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e3 (op e2 e2))) (= e5 (op e1 e1))) (= e1 (op e4 e3))) (= e4 (op e3 e2)))))
+(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e3 (op e2 e2))) (= e5 (op e4 e4))) (= e4 (op e1 e3))) (= e1 (op e3 e2)))))
+(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e4 (op e2 e2))) (= e1 (op e3 e3))) (= e3 (op e5 e4))) (= e5 (op e4 e2)))))
+(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e4 (op e2 e2))) (= e1 (op e5 e5))) (= e5 (op e3 e4))) (= e3 (op e4 e2)))))
+(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e4 (op e2 e2))) (= e3 (op e1 e1))) (= e1 (op e5 e4))) (= e5 (op e4 e2)))))
+(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e4 (op e2 e2))) (= e3 (op e5 e5))) (= e5 (op e1 e4))) (= e1 (op e4 e2)))))
+(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e4 (op e2 e2))) (= e5 (op e1 e1))) (= e1 (op e3 e4))) (= e3 (op e4 e2)))))
+(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e4 (op e2 e2))) (= e5 (op e3 e3))) (= e3 (op e1 e4))) (= e1 (op e4 e2)))))
+(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e5 (op e2 e2))) (= e1 (op e3 e3))) (= e3 (op e4 e5))) (= e4 (op e5 e2)))))
+(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e5 (op e2 e2))) (= e1 (op e4 e4))) (= e4 (op e3 e5))) (= e3 (op e5 e2)))))
+(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e5 (op e2 e2))) (= e3 (op e1 e1))) (= e1 (op e4 e5))) (= e4 (op e5 e2)))))
+(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e5 (op e2 e2))) (= e3 (op e4 e4))) (= e4 (op e1 e5))) (= e1 (op e5 e2)))))
+(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e5 (op e2 e2))) (= e4 (op e1 e1))) (= e1 (op e3 e5))) (= e3 (op e5 e2)))))
+(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e5 (op e2 e2))) (= e4 (op e3 e3))) (= e3 (op e1 e5))) (= e1 (op e5 e2)))))
+(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e1 (op e3 e3))) (= e2 (op e4 e4))) (= e4 (op e5 e1))) (= e5 (op e1 e3)))))
+(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e1 (op e3 e3))) (= e2 (op e5 e5))) (= e5 (op e4 e1))) (= e4 (op e1 e3)))))
+(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e1 (op e3 e3))) (= e4 (op e2 e2))) (= e2 (op e5 e1))) (= e5 (op e1 e3)))))
+(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e1 (op e3 e3))) (= e4 (op e5 e5))) (= e5 (op e2 e1))) (= e2 (op e1 e3)))))
+(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e1 (op e3 e3))) (= e5 (op e2 e2))) (= e2 (op e4 e1))) (= e4 (op e1 e3)))))
+(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e1 (op e3 e3))) (= e5 (op e4 e4))) (= e4 (op e2 e1))) (= e2 (op e1 e3)))))
+(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e2 (op e3 e3))) (= e1 (op e4 e4))) (= e4 (op e5 e2))) (= e5 (op e2 e3)))))
+(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e2 (op e3 e3))) (= e1 (op e5 e5))) (= e5 (op e4 e2))) (= e4 (op e2 e3)))))
+(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e2 (op e3 e3))) (= e4 (op e1 e1))) (= e1 (op e5 e2))) (= e5 (op e2 e3)))))
+(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e2 (op e3 e3))) (= e4 (op e5 e5))) (= e5 (op e1 e2))) (= e1 (op e2 e3)))))
+(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e2 (op e3 e3))) (= e5 (op e1 e1))) (= e1 (op e4 e2))) (= e4 (op e2 e3)))))
+(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e2 (op e3 e3))) (= e5 (op e4 e4))) (= e4 (op e1 e2))) (= e1 (op e2 e3)))))
+(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e4 (op e3 e3))) (= e1 (op e2 e2))) (= e2 (op e5 e4))) (= e5 (op e4 e3)))))
+(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e4 (op e3 e3))) (= e1 (op e5 e5))) (= e5 (op e2 e4))) (= e2 (op e4 e3)))))
+(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e4 (op e3 e3))) (= e2 (op e1 e1))) (= e1 (op e5 e4))) (= e5 (op e4 e3)))))
+(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e4 (op e3 e3))) (= e2 (op e5 e5))) (= e5 (op e1 e4))) (= e1 (op e4 e3)))))
+(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e4 (op e3 e3))) (= e5 (op e1 e1))) (= e1 (op e2 e4))) (= e2 (op e4 e3)))))
+(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e4 (op e3 e3))) (= e5 (op e2 e2))) (= e2 (op e1 e4))) (= e1 (op e4 e3)))))
+(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e5 (op e3 e3))) (= e1 (op e2 e2))) (= e2 (op e4 e5))) (= e4 (op e5 e3)))))
+(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e5 (op e3 e3))) (= e1 (op e4 e4))) (= e4 (op e2 e5))) (= e2 (op e5 e3)))))
+(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e5 (op e3 e3))) (= e2 (op e1 e1))) (= e1 (op e4 e5))) (= e4 (op e5 e3)))))
+(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e5 (op e3 e3))) (= e2 (op e4 e4))) (= e4 (op e1 e5))) (= e1 (op e5 e3)))))
+(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e5 (op e3 e3))) (= e4 (op e1 e1))) (= e1 (op e2 e5))) (= e2 (op e5 e3)))))
+(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e5 (op e3 e3))) (= e4 (op e2 e2))) (= e2 (op e1 e5))) (= e1 (op e5 e3)))))
+(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e1 (op e4 e4))) (= e2 (op e3 e3))) (= e3 (op e5 e1))) (= e5 (op e1 e4)))))
+(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e1 (op e4 e4))) (= e2 (op e5 e5))) (= e5 (op e3 e1))) (= e3 (op e1 e4)))))
+(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e1 (op e4 e4))) (= e3 (op e2 e2))) (= e2 (op e5 e1))) (= e5 (op e1 e4)))))
+(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e1 (op e4 e4))) (= e3 (op e5 e5))) (= e5 (op e2 e1))) (= e2 (op e1 e4)))))
+(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e1 (op e4 e4))) (= e5 (op e2 e2))) (= e2 (op e3 e1))) (= e3 (op e1 e4)))))
+(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e1 (op e4 e4))) (= e5 (op e3 e3))) (= e3 (op e2 e1))) (= e2 (op e1 e4)))))
+(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e2 (op e4 e4))) (= e1 (op e3 e3))) (= e3 (op e5 e2))) (= e5 (op e2 e4)))))
+(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e2 (op e4 e4))) (= e1 (op e5 e5))) (= e5 (op e3 e2))) (= e3 (op e2 e4)))))
+(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e2 (op e4 e4))) (= e3 (op e1 e1))) (= e1 (op e5 e2))) (= e5 (op e2 e4)))))
+(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e2 (op e4 e4))) (= e3 (op e5 e5))) (= e5 (op e1 e2))) (= e1 (op e2 e4)))))
+(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e2 (op e4 e4))) (= e5 (op e1 e1))) (= e1 (op e3 e2))) (= e3 (op e2 e4)))))
+(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e2 (op e4 e4))) (= e5 (op e3 e3))) (= e3 (op e1 e2))) (= e1 (op e2 e4)))))
+(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e3 (op e4 e4))) (= e1 (op e2 e2))) (= e2 (op e5 e3))) (= e5 (op e3 e4)))))
+(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e3 (op e4 e4))) (= e1 (op e5 e5))) (= e5 (op e2 e3))) (= e2 (op e3 e4)))))
+(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e3 (op e4 e4))) (= e2 (op e1 e1))) (= e1 (op e5 e3))) (= e5 (op e3 e4)))))
+(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e3 (op e4 e4))) (= e2 (op e5 e5))) (= e5 (op e1 e3))) (= e1 (op e3 e4)))))
+(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e3 (op e4 e4))) (= e5 (op e1 e1))) (= e1 (op e2 e3))) (= e2 (op e3 e4)))))
+(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e3 (op e4 e4))) (= e5 (op e2 e2))) (= e2 (op e1 e3))) (= e1 (op e3 e4)))))
+(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e5 (op e4 e4))) (= e1 (op e2 e2))) (= e2 (op e3 e5))) (= e3 (op e5 e4)))))
+(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e5 (op e4 e4))) (= e1 (op e3 e3))) (= e3 (op e2 e5))) (= e2 (op e5 e4)))))
+(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e5 (op e4 e4))) (= e2 (op e1 e1))) (= e1 (op e3 e5))) (= e3 (op e5 e4)))))
+(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e5 (op e4 e4))) (= e2 (op e3 e3))) (= e3 (op e1 e5))) (= e1 (op e5 e4)))))
+(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e5 (op e4 e4))) (= e3 (op e1 e1))) (= e1 (op e2 e5))) (= e2 (op e5 e4)))))
+(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e5 (op e4 e4))) (= e3 (op e2 e2))) (= e2 (op e1 e5))) (= e1 (op e5 e4)))))
+(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e1 (op e5 e5))) (= e2 (op e3 e3))) (= e3 (op e4 e1))) (= e4 (op e1 e5)))))
+(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e1 (op e5 e5))) (= e2 (op e4 e4))) (= e4 (op e3 e1))) (= e3 (op e1 e5)))))
+(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e1 (op e5 e5))) (= e3 (op e2 e2))) (= e2 (op e4 e1))) (= e4 (op e1 e5)))))
+(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e1 (op e5 e5))) (= e3 (op e4 e4))) (= e4 (op e2 e1))) (= e2 (op e1 e5)))))
+(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e1 (op e5 e5))) (= e4 (op e2 e2))) (= e2 (op e3 e1))) (= e3 (op e1 e5)))))
+(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e1 (op e5 e5))) (= e4 (op e3 e3))) (= e3 (op e2 e1))) (= e2 (op e1 e5)))))
+(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e2 (op e5 e5))) (= e1 (op e3 e3))) (= e3 (op e4 e2))) (= e4 (op e2 e5)))))
+(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e2 (op e5 e5))) (= e1 (op e4 e4))) (= e4 (op e3 e2))) (= e3 (op e2 e5)))))
+(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e2 (op e5 e5))) (= e3 (op e1 e1))) (= e1 (op e4 e2))) (= e4 (op e2 e5)))))
+(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e2 (op e5 e5))) (= e3 (op e4 e4))) (= e4 (op e1 e2))) (= e1 (op e2 e5)))))
+(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e2 (op e5 e5))) (= e4 (op e1 e1))) (= e1 (op e3 e2))) (= e3 (op e2 e5)))))
+(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e2 (op e5 e5))) (= e4 (op e3 e3))) (= e3 (op e1 e2))) (= e1 (op e2 e5)))))
+(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e3 (op e5 e5))) (= e1 (op e2 e2))) (= e2 (op e4 e3))) (= e4 (op e3 e5)))))
+(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e3 (op e5 e5))) (= e1 (op e4 e4))) (= e4 (op e2 e3))) (= e2 (op e3 e5)))))
+(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e3 (op e5 e5))) (= e2 (op e1 e1))) (= e1 (op e4 e3))) (= e4 (op e3 e5)))))
+(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e3 (op e5 e5))) (= e2 (op e4 e4))) (= e4 (op e1 e3))) (= e1 (op e3 e5)))))
+(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e3 (op e5 e5))) (= e4 (op e1 e1))) (= e1 (op e2 e3))) (= e2 (op e3 e5)))))
+(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e3 (op e5 e5))) (= e4 (op e2 e2))) (= e2 (op e1 e3))) (= e1 (op e3 e5)))))
+(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e4 (op e5 e5))) (= e1 (op e2 e2))) (= e2 (op e3 e4))) (= e3 (op e4 e5)))))
+(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e4 (op e5 e5))) (= e1 (op e3 e3))) (= e3 (op e2 e4))) (= e2 (op e4 e5)))))
+(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e4 (op e5 e5))) (= e2 (op e1 e1))) (= e1 (op e3 e4))) (= e3 (op e4 e5)))))
+(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e4 (op e5 e5))) (= e2 (op e3 e3))) (= e3 (op e1 e4))) (= e1 (op e4 e5)))))
+(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e4 (op e5 e5))) (= e3 (op e1 e1))) (= e1 (op e2 e4))) (= e2 (op e4 e5)))))
+(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e4 (op e5 e5))) (= e3 (op e2 e2))) (= e2 (op e1 e4))) (= e1 (op e4 e5)))))
+(check-sat)
+(exit)
--- /dev/null
+#!/bin/bash
+# Simple pidgeon-hole problem generator in SMT-LIBv2
+# (c) 2011 Morgan Deters <mdeters@cs.nyu.edu>
+# 2011 July 7
+
+if [ $# -ne 1 ]; then
+ echo "usage: $(basename "$0") size" >&2
+ exit 1
+fi
+
+N=$1
+
+echo "(set-logic QF_UF)"
+echo "(declare-sort U 0)"
+
+i=1; while [ $i -le $N ]; do
+ echo "(declare-fun p_$i () U)"
+ let ++i
+done
+
+i=1; while [ $i -le $(($N-1)) ]; do
+ echo "(declare-fun h_$i () U)"
+ let ++i
+done
+
+i=1; while [ $i -le $(($N-1)) ]; do
+ j=$(($i+1)); while [ $j -le $N ]; do
+ echo "(assert (not (= p_$i p_$j)))"
+ let ++j
+ done
+ let ++i
+done
+
+i=1; while [ $i -le $N ]; do
+ echo -n "(assert (or"
+ j=1; while [ $j -le $(($N-1)) ]; do
+ echo -n " (= p_$i h_$j)"
+ let ++j
+ done
+ echo "))"
+ let ++i
+done
+
+echo "(check-sat)"
projects / cvc5.git / commitdiff