cout << " -> ";
translate_to_isat(variables, assertion[1]);
cout << ")";
- break;
- case kind::IFF:
- cout << "(";
- translate_to_isat(variables, assertion[0]);
- cout << " <-> ";
- translate_to_isat(variables, assertion[1]);
- cout << ")";
- break;
+ break;
case kind::EQUAL:
- op = "=";
- theory = true;
- break;
+ if( assertion[0].getType().isBoolean() ){
+ cout << "(";
+ translate_to_isat(variables, assertion[0]);
+ cout << " <-> ";
+ translate_to_isat(variables, assertion[1]);
+ cout << ")";
+ }else{
+ op = "=";
+ theory = true;
+ }
+ break;
case kind::LT:
op = "<";
theory = true;
cout << ",";
translate_to_mathematica(variables, assertion[1]);
cout << "]";
- break;
- case kind::IFF:
+ break;
+ case kind::EQUAL:
+ if( assertion[0].getType().isBoolean() ){
cout << "Equivalent[";
translate_to_mathematica(variables, assertion[0]);
cout << ",";
translate_to_mathematica(variables, assertion[1]);
cout << "]";
- break;
- case kind::EQUAL:
+ }else{
op = "==";
theory = true;
- break;
+ }
+ break;
case kind::LT:
op = "<";
theory = true;
op = "==>";
binary = true;
break;
- case kind::IFF:
- op = "<==>";
- binary = true;
- break;
case kind::EQUAL:
- op = "=";
- theory = true;
- break;
+ if( assertion[0].getType().isBoolean() ){
+ op = "<==>";
+ binary = true;
+ }else{
+ op = "=";
+ theory = true;
+ }
+ break;
case kind::LT:
op = "<";
theory = true;
cout << " impl ";
translate_to_redlog(variables, assertion[1]);
cout << ")";
- break;
- case kind::IFF:
- cout << "(";
- translate_to_redlog(variables, assertion[0]);
- cout << " equiv ";
- translate_to_redlog(variables, assertion[1]);
- cout << ")";
- break;
+ break;
case kind::EQUAL:
- op = "=";
- theory = true;
- break;
+ if( assertion[0].getType().isBoolean() ){
+ cout << "(";
+ translate_to_redlog(variables, assertion[0]);
+ cout << " equiv ";
+ translate_to_redlog(variables, assertion[1]);
+ cout << ")";
+ }else{
+ op = "=";
+ theory = true;
+ }
+ break;
case kind::LT:
op = "<";
theory = true;
}
Expr Expr::iffExpr(const Expr& right) const {
- return getEM()->mkExpr(CVC4::kind::IFF, *this, right);
+ return getEM()->mkExpr(CVC4::kind::EQUAL, *this, right);
}
Expr Expr::impExpr(const Expr& right) const {
case CVC4::kind::AND:
case CVC4::kind::OR:
case CVC4::kind::ITE:
- case CVC4::kind::IFF:
case CVC4::kind::IMPLIES:
return false;
+ case CVC4::kind::EQUAL:
+ return (*this)[0].getType().isBool();
+ break;
default:
; /* fall through */
}
case CVC4::kind::AND:
case CVC4::kind::OR:
case CVC4::kind::IMPLIES:
- case CVC4::kind::IFF:
case CVC4::kind::XOR:
case CVC4::kind::ITE:
return true;
+ case CVC4::kind::EQUAL:
+ return (*this)[0].getType().isBool();
+ break;
default:
return false;
}
}
bool Expr::isIff() const {
- return getKind() == CVC4::kind::IFF;
+ return getKind() == CVC4::kind::EQUAL && (*this)[0].getType().isBool();;
}
bool Expr::isImpl() const {
}
Expr ValidityChecker::iffExpr(const Expr& left, const Expr& right) {
- return d_em->mkExpr(CVC4::kind::IFF, left, right);
+ return d_em->mkExpr(CVC4::kind::EQUAL, left, right);
}
Expr ValidityChecker::eqExpr(const Expr& child0, const Expr& child1) {
inline void computeXorIffDesiredValues
(Kind k, SatValue desiredVal, SatValue &desiredVal1, SatValue &desiredVal2)
{
- Assert(k == kind::IFF || k == kind::XOR);
+ Assert(k == kind::EQUAL || k == kind::XOR);
bool shouldInvert =
- (desiredVal == SAT_VALUE_TRUE && k == kind::IFF) ||
+ (desiredVal == SAT_VALUE_TRUE && k == kind::EQUAL) ||
(desiredVal == SAT_VALUE_FALSE && k == kind::XOR);
if(desiredVal1 == SAT_VALUE_UNKNOWN &&
/* What type of node is this */
Kind k = node.getKind();
theory::TheoryId tId = theory::kindToTheoryId(k);
+ bool isAtom =
+ (k == kind::BOOLEAN_TERM_VARIABLE ) ||
+ ( (tId != theory::THEORY_BOOL) &&
+ (k != kind::EQUAL || (!node[0].getType().isBoolean())) );
/* Some debugging stuff */
Debug("decision::jh") << "kind = " << k << std::endl
/**
* If not in theory of booleans, check if this is something to split-on.
*/
- if(tId != theory::THEORY_BOOL) {
+ if(isAtom) {
// if node has embedded ites, resolve that first
if(handleEmbeddedITEs(node) == FOUND_SPLITTER)
return FOUND_SPLITTER;
break;
case kind::XOR:
- case kind::IFF: {
+ case kind::EQUAL: {
SatValue desiredVal1 = tryGetSatValue(node[0]);
SatValue desiredVal2 = tryGetSatValue(node[1]);
computeXorIffDesiredValues(k, desiredVal, desiredVal1, desiredVal2);
"Don't have an expression manager for this expression!");
PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
"Different expression managers!");
- return d_exprManager->mkExpr(IFF, *this, e);
+ return d_exprManager->mkExpr(EQUAL, *this, e);
}
Expr Expr::impExpr(const Expr& e) const {
NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart,
const NodeTemplate<ref_count3>& elsepart) const;
template <bool ref_count2>
- NodeTemplate<true> iffNode(const NodeTemplate<ref_count2>& right) const;
- template <bool ref_count2>
NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const;
template <bool ref_count2>
NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const;
return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
}
-template <bool ref_count>
-template <bool ref_count2>
-NodeTemplate<true>
-NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count2>& right) const {
- assertTNodeNotExpired();
- return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
-}
-
template <bool ref_count>
template <bool ref_count2>
NodeTemplate<true>
return n;
}
+Node NodeManager::mkBooleanTermVariable() {
+ Node n = NodeBuilder<0>(this, kind::BOOLEAN_TERM_VARIABLE);
+ n.setAttribute(TypeAttr(), booleanType());
+ n.setAttribute(TypeCheckedAttr(), true);
+ return n;
+}
+
Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) {
std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type );
if( it==d_unique_vars[k].end() ){
/** Create a instantiation constant with the given type. */
Node mkInstConstant(const TypeNode& type);
+
+ /** Create a boolean term variable. */
+ Node mkBooleanTermVariable();
/** Make a new abstract value with the given type. */
Node mkAbstractValue(const TypeNode& type);
namespace CVC4 {
-std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) {
- switch(mode) {
- case theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
- out << "BOOLEAN_TERM_CONVERT_TO_BITVECTORS";
- break;
- case theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
- out << "BOOLEAN_TERM_CONVERT_TO_DATATYPES";
- break;
- case theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE:
- out << "BOOLEAN_TERM_CONVERT_NATIVE";
- break;
- default:
- out << "BooleanTermConversionMode!UNKNOWN";
- }
-
- return out;
-}
}/* CVC4 namespace */
namespace theory {
namespace booleans {
-enum BooleanTermConversionMode {
- /**
- * Convert Boolean terms to bitvectors of size 1.
- */
- BOOLEAN_TERM_CONVERT_TO_BITVECTORS,
- /**
- * Convert Boolean terms to enumerations in the Datatypes theory.
- */
- BOOLEAN_TERM_CONVERT_TO_DATATYPES,
- /**
- * Convert Boolean terms to enumerations in the Datatypes theory IF
- * used in a datatypes context, otherwise to a bitvector of size 1.
- */
- BOOLEAN_TERM_CONVERT_NATIVE
-
-};
-
}/* CVC4::theory::booleans namespace */
}/* CVC4::theory namespace */
-std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) CVC4_PUBLIC;
-
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */
module BOOLEANS "options/booleans_options.h" Boolean theory
-option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "options/boolean_term_conversion_mode.h" :handler stringToBooleanTermConversionMode
- policy for converting Boolean terms
endmodule
option typeChecking type-checking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking
never type check expressions
-option biasedITERemoval --biased-ites bool :default false
- try the new remove ite pass that is biased against term ites appearing
-
endmodule
}
}
-
-// theory/booleans/options_handlers.h
-const std::string OptionsHandler::s_booleanTermConversionModeHelp = "\
-Boolean term conversion modes currently supported by the\n\
---boolean-term-conversion-mode option:\n\
-\n\
-bitvectors [default]\n\
-+ Boolean terms are converted to bitvectors of size 1.\n\
-\n\
-datatypes\n\
-+ Boolean terms are converted to enumerations in the Datatype theory.\n\
-\n\
-native\n\
-+ Boolean terms are converted in a \"natural\" way depending on where they\n\
- are used. If in a datatype context, they are converted to an enumeration.\n\
- Elsewhere, they are converted to a bitvector of size 1.\n\
-";
-
-theory::booleans::BooleanTermConversionMode OptionsHandler::stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException){
- if(optarg == "bitvectors") {
- return theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS;
- } else if(optarg == "datatypes") {
- return theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES;
- } else if(optarg == "native") {
- return theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE;
- } else if(optarg == "help") {
- puts(s_booleanTermConversionModeHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") +
- optarg + "'. Try --boolean-term-conversion-mode help.");
- }
-}
-
-
// theory/uf/options_handlers.h
const std::string OptionsHandler::s_ufssModeHelp = "\
UF strong solver options currently supported by the --uf-ss option:\n\
theory::bv::SatSolverMode stringToSatSolver(std::string option, std::string optarg) throw(OptionException);
-
- // theory/booleans/options_handlers.h
- theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException);
-
// theory/uf/options_handlers.h
theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg) throw(OptionException);
switch(type) {
// booleanBinop
- case IFF_TOK: return kind::IFF;
+ case IFF_TOK: return kind::EQUAL;
case IMPLIES_TOK: return kind::IMPLIES;
case OR_TOK: return kind::OR;
case XOR_TOK: return kind::XOR;
Expr rhs = createPrecedenceTree(parser, em, expressions, operators, pivot + 1, stopIndex);
switch(k) {
- case kind::EQUAL: {
- if(lhs.getType().isBoolean()) {
- if(parser->strictModeEnabled()) {
- WarningOnce() << "Warning: in strict parsing mode, will not convert BOOL = BOOL to BOOL <=> BOOL" << std::endl;
- } else {
- k = kind::IFF;
- }
- }
- break;
- }
case kind::LEQ : if(lhs.getType().isSet()) { k = kind::SUBSET; } break;
case kind::MINUS : if(lhs.getType().isSet()) { k = kind::SETMINUS; } break;
case kind::BITVECTOR_AND: if(lhs.getType().isSet()) { k = kind::INTERSECTION; } break;
| AND_TOK { $kind = CVC4::kind::AND; }
| OR_TOK { $kind = CVC4::kind::OR; }
| XOR_TOK { $kind = CVC4::kind::XOR; }
- | IFF_TOK { $kind = CVC4::kind::IFF; }
+ | IFF_TOK { $kind = CVC4::kind::EQUAL; }
| EQUAL_TOK { $kind = CVC4::kind::EQUAL; }
| DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
// Arithmetic
// Boolean symbols are always defined
addOperator(kind::AND);
addOperator(kind::EQUAL);
- addOperator(kind::IFF);
addOperator(kind::IMPLIES);
addOperator(kind::ITE);
addOperator(kind::NOT);
//set the attribute to denote this is a function definition
seq->addCommand( new SetUserAttributeCommand( attr_name, func_app ) );
//assert it
- Expr equality = MK_EXPR( func_app.getType().isBoolean() ?
- kind::IFF : kind::EQUAL, func_app, expr);
+ Expr equality = MK_EXPR( kind::EQUAL, func_app, expr);
Expr boundVars = EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs);
Expr as = EXPR_MANAGER->mkExpr(kind::FORALL, boundVars, equality, aexpr);
seq->addCommand( new AssertCommand(as, false) );
Expr as = EXPR_MANAGER->mkExpr(
kind::FORALL,
EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs),
- MK_EXPR( func_app.getType().isBoolean() ?
- kind::IFF : kind::EQUAL, func_app, expr ),
+ MK_EXPR( kind::EQUAL, func_app, expr ),
aexpr);
seq->addCommand( new AssertCommand(as, false) );
//set up the next scope
: /* a built-in operator application */
LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
{
- if( kind == CVC4::kind::EQUAL &&
- args.size() > 0 &&
- args[0].getType() == EXPR_MANAGER->booleanType() ) {
- /* Use IFF for boolean equalities. */
- kind = CVC4::kind::IFF;
- }
-
if( !PARSER_STATE->strictModeEnabled() &&
(kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
args.size() == 1) {
for(size_t i = args.size() - 1; i > 0;) {
expr = MK_EXPR(kind, args[--i], expr);
}
- } else if( ( kind == CVC4::kind::IFF || kind == CVC4::kind::EQUAL ||
+ } else if( ( kind == CVC4::kind::EQUAL ||
kind == CVC4::kind::LT || kind == CVC4::kind::GT ||
kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) &&
args.size() > 2 ) {
Expr guard;
Expr body;
if(expr[1].getKind() == kind::IMPLIES ||
- expr[1].getKind() == kind::IFF ||
expr[1].getKind() == kind::EQUAL) {
guard = expr[0];
body = expr[1];
args.push_back(f2);
}
- if ( body.getKind()==kind::IMPLIES ) kind = kind::RR_DEDUCTION;
- else if( body.getKind()==kind::IFF ) kind = kind::RR_REDUCTION;
- else if( body.getKind()==kind::EQUAL ) kind = kind::RR_REWRITE;
- else PARSER_STATE->parseError("Error parsing rewrite rule.");
-
+ if( body.getKind()==kind::IMPLIES ){
+ kind = kind::RR_DEDUCTION;
+ }else if( body.getKind()==kind::EQUAL ){
+ kind = body[0].getType().isBoolean() ? kind::RR_REDUCTION : kind::RR_REWRITE;
+ }else{
+ PARSER_STATE->parseError("Error parsing rewrite rule.");
+ }
expr = MK_EXPR( kind, args );
} else if(! patexprs.empty()) {
if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){
std::string attr_name = attr;
attr_name.erase( attr_name.begin() );
if( attr==":fun-def" ){
- if( ( expr.getKind()!=kind::EQUAL && expr.getKind()!=kind::IFF ) ||
- expr[0].getKind()!=kind::APPLY_UF ){
+ if( expr.getKind()!=kind::EQUAL || expr[0].getKind()!=kind::APPLY_UF ){
success = false;
}else{
FunctionType t = (FunctionType)expr[0].getOperator().getType();
Parser::addOperator(kind::AND);
Parser::addOperator(kind::DISTINCT);
Parser::addOperator(kind::EQUAL);
- Parser::addOperator(kind::IFF);
Parser::addOperator(kind::IMPLIES);
Parser::addOperator(kind::ITE);
Parser::addOperator(kind::NOT);
oldKind = kind::MINUS;
newKind = kind::UMINUS;
}
+ /*
//convert to IFF if boolean EQUAL
if( sgt.d_expr==getExprManager()->operatorOf(kind::EQUAL) ){
Type ctn = sgt.d_children[0].d_type;
newKind = kind::IFF;
}
}
+ */
if( newKind!=kind::UNDEFINED_KIND ){
Expr newExpr = getExprManager()->operatorOf(newKind);
Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl;
}
}
Debug("parser-sygus") << "...made built term " << builtTerm << std::endl;
- Expr assertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
+ Expr assertion = getExprManager()->mkExpr(kind::EQUAL, evalApply, builtTerm);
if( !bvl.isNull() ){
Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern);
Debug("parser-sygus") << "builtApply " << builtApply[k] << std::endl;
builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
Debug("parser-sygus") << "builtTerm " << builtTerm << std::endl;
- Expr eassertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
+ Expr eassertion = getExprManager()->mkExpr(kind::EQUAL, evalApply, builtTerm);
Expr epattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
epattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, epattern);
eassertion = getExprManager()->mkExpr(kind::FORALL, nbvl, eassertion, epattern);
( fofBinaryNonAssoc[na] fofUnitaryFormula[expr2]
{ switch(na) {
case tptp::NA_IFF:
- expr = MK_EXPR(kind::IFF,expr,expr2);
+ expr = MK_EXPR(kind::EQUAL,expr,expr2);
break;
case tptp::NA_REVIFF:
expr = MK_EXPR(kind::XOR,expr,expr2);
( fofBinaryNonAssoc[na] tffUnitaryFormula[expr2]
{ switch(na) {
case tptp::NA_IFF:
- expr = MK_EXPR(kind::IFF,expr,expr2);
+ expr = MK_EXPR(kind::EQUAL,expr,expr2);
break;
case tptp::NA_REVIFF:
expr = MK_EXPR(kind::XOR,expr,expr2);
defineVar("$false", em->mkConst(false));
addOperator(kind::AND);
addOperator(kind::EQUAL);
- addOperator(kind::IFF);
addOperator(kind::IMPLIES);
//addOperator(kind::ITE); //only for tff thf
addOperator(kind::NOT);
// BUILTIN
case kind::EQUAL:
- op << '=';
+ if( n[0].getType().isBoolean() ){
+ op << "<=>";
+ }else{
+ op << '=';
+ }
opType = INFIX;
break;
case kind::ITE:
op << "XOR";
opType = INFIX;
break;
- case kind::IFF:
- op << "<=>";
- opType = INFIX;
- break;
case kind::IMPLIES:
op << "=>";
opType = INFIX;
// bool theory
case kind::NOT:
case kind::AND:
- case kind::IFF:
case kind::IMPLIES:
case kind::OR:
case kind::XOR:
// bool theory
case kind::NOT: return "not";
case kind::AND: return "and";
- case kind::IFF: return "=";
case kind::IMPLIES: return "=>";
case kind::OR: return "or";
case kind::XOR: return "xor";
namespace CVC4 {
inline static Node eqNode(TNode n1, TNode n2) {
- return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2);
+ return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2);
}
// congrence matching term helper
// we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs
// b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof,
// and use it to determine which option we need.
- if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) {
+ if(n2.getKind() == kind::EQUAL) {
if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) {
// We are in a sequence of identical equalities
} else {
// We have a "next node". Use it to guide us.
- Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL ||
- nodeAfterEqualitySequence.getKind() == kind::IFF);
+ Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL);
if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) {
Debug("pf::arith") << "\ndoing trans proof, got n2 " << n2 << "\n";
if(tb == 1) {
Debug("pf::arith") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n";
- Debug("pf::arith") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n";
+ Debug("pf::arith") << (n2.getKind() == kind::EQUAL) << "\n";
if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) {
Debug("pf::arith") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n";
}
ss << "(trans _ _ _ _ ";
- if((n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) &&
- (n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF))
+ if((n2.getKind() == kind::EQUAL) && (n1.getKind() == kind::EQUAL))
// Both elements of the transitivity rule are equalities/iffs
{
if(n1[0] == n2[0]) {
Unreachable();
}
Debug("pf::arith") << "++ trans proof[" << i << "], now have " << n1 << std::endl;
- } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) {
+ } else if(n1.getKind() == kind::EQUAL) {
// n1 is an equality/iff, but n2 is a predicate
if(n1[0] == n2) {
n1 = n1[1];
} else {
Unreachable();
}
- } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) {
+ } else if(n2.getKind() == kind::EQUAL) {
// n2 is an equality/iff, but n1 is a predicate
if(n2[0] == n1) {
n1 = n2[1];
namespace CVC4 {
inline static Node eqNode(TNode n1, TNode n2) {
- return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2);
+ return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2);
}
// congrence matching term helper
// b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof,
// and use it to determine which option we need.
- if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) {
+ if(n2.getKind() == kind::EQUAL) {
if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) {
// We are in a sequence of identical equalities
nodeAfterEqualitySequence = nodeAfterEqualitySequence[0];
}
- Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL ||
- nodeAfterEqualitySequence.getKind() == kind::IFF);
+ Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL);
if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) {
Debug("mgd") << "\ndoing trans proof, got n2 " << n2 << "\n";
if(tb == 1) {
Debug("mgdx") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n";
- Debug("mgdx") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n";
+ Debug("mgdx") << (n2.getKind() == kind::EQUAL) << "\n";
if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) {
Debug("mgdx") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n";
ss << "(trans _ _ _ _ ";
}
- if((n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) &&
- (n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF))
+ if((n2.getKind() == kind::EQUAL) && (n1.getKind() == kind::EQUAL))
// Both elements of the transitivity rule are equalities/iffs
{
if(n1[0] == n2[0]) {
Unreachable();
}
Debug("mgd") << "++ trans proof[" << i << "], now have " << n1 << std::endl;
- } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) {
+ } else if(n1.getKind() == kind::EQUAL) {
// n1 is an equality/iff, but n2 is a predicate
if(n1[0] == n2) {
n1 = n1[1];
} else {
Unreachable();
}
- } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) {
+ } else if(n2.getKind() == kind::EQUAL) {
// n2 is an equality/iff, but n1 is a predicate
if(n2[0] == n1) {
n1 = n2[1];
}
void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map) {
- std::string op = utils::toLFSCKind(term.getKind());
+ std::string op = utils::toLFSCKindTerm(term);
std::ostringstream paren;
std::string holes = term.getKind() == kind::BITVECTOR_CONCAT ? "_ _ " : "";
unsigned size = term.getKind() == kind::BITVECTOR_CONCAT? utils::getSize(term) :
void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map) {
os <<"(";
- os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" ";
+ os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" ";
os << " ";
d_proofEngine->printBoundTerm(term[0], os, map);
os <<")";
void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const ProofLetMap& map) {
os <<"(";
- os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term[0]) <<" ";
+ os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term[0]) <<" ";
os << " ";
d_proofEngine->printBoundTerm(term[0], os, map);
os << " ";
void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map) {
os <<"(";
- os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" ";
+ os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" ";
os <<" ";
if (term.getKind() == kind::BITVECTOR_REPEAT) {
unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount;
case kind::EQUAL: {
Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl;
- os << "(bv_bbl_" << utils::toLFSCKind(atom.getKind());
+ os << "(bv_bbl_" << utils::toLFSCKindTerm(atom);
if (swap) {os << "_swap";}
os << ")";
}
}
- }else if( base_assertion.getKind()==kind::XOR || base_assertion.getKind()==kind::IFF ){
+ }else if( base_assertion.getKind()==kind::XOR || ( base_assertion.getKind()==kind::EQUAL && base_assertion[0].getType().isBoolean() ) ){
//eliminate negation
int num_nots_2 = 0;
int num_nots_1 = 0;
Kind k;
if( !base_pol ){
- if( base_assertion.getKind()==kind::IFF ){
+ if( base_assertion.getKind()==kind::EQUAL ){
num_nots_2 = 1;
}
- k = kind::IFF;
+ k = kind::EQUAL;
}else{
k = base_assertion.getKind();
}
if( i==0 ){
//figure out which way to elim
elimNum = child_pol==childPol[child_base] ? 2 : 1;
- if( (elimNum==2)==(k==kind::IFF) ){
+ if( (elimNum==2)==(k==kind::EQUAL) ){
num_nots_2++;
}
if( elimNum==1 ){
os_base_n << ProofManager::getLitName(lit1, d_name) << " ";
}
Assert( elimNum!=0 );
- os_base_n << "(" << ( k==kind::IFF ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ ";
+ os_base_n << "(" << ( k==kind::EQUAL ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ ";
if( !base_pol ){
- os_base_n << "(not_" << ( base_assertion.getKind()==kind::IFF ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")";
+ os_base_n << "(not_" << ( base_assertion.getKind()==kind::EQUAL ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")";
}else{
os_base_n << os_base.str();
}
case kind::AND: return "and";
case kind::XOR: return "xor";
case kind::EQUAL: return "=";
- case kind::IFF: return "iff";
case kind::IMPLIES: return "impl";
case kind::NOT: return "not";
}
}
+std::string toLFSCKindTerm(Expr node) {
+ Kind k = node.getKind();
+ if( k==kind::EQUAL ){
+ if( node[0].getType().isBoolean() ){
+ return "iff";
+ }else{
+ return "=";
+ }
+ }else{
+ return toLFSCKind( k );
+ }
+}
+
} /* namespace CVC4::utils */
} /* namespace CVC4 */
namespace utils {
std::string toLFSCKind(Kind kind);
+std::string toLFSCKindTerm(Expr node);
inline unsigned getExtractHigh(Expr node) {
return node.getOperator().getConst<BitVectorExtract>().high;
case kind::EQUAL:
os << "(";
- os << "= ";
- printSort(term[0].getType(), os);
- os << " ";
+ if( term[0].getType().isBoolean() ){
+ os << "iff ";
+ }else{
+ os << "= ";
+ printSort(term[0].getType(), os);
+ os << " ";
+ }
printBoundTerm(term[0], os, map);
os << " ";
printBoundTerm(term[1], os, map);
// LFSC doesn't allow declarations with variable numbers of
// arguments, so we have to flatten chained operators, like =.
Kind op = term.getOperator().getConst<Chain>().getOperator();
+ std::string op_str;
+ if( op==kind::EQUAL && term[0].getType().isBoolean() ){
+ op_str = "iff";
+ }else{
+ op_str = utils::toLFSCKind(op);
+ }
size_t n = term.getNumChildren();
std::ostringstream paren;
for(size_t i = 1; i < n; ++i) {
os << "(" << utils::toLFSCKind(kind::AND) << " ";
paren << ")";
}
- os << "(" << utils::toLFSCKind(op) << " ";
+ os << "(" << op_str << " ";
printBoundTerm(term[i - 1], os, map);
os << " ";
printBoundTerm(term[i], os, map);
// If letification is off or there were 2 children, same treatment as the other cases.
// (No break is intentional).
case kind::XOR:
- case kind::IFF:
case kind::IMPLIES:
case kind::NOT:
// print the Boolean operators
namespace CVC4 {
inline static Node eqNode(TNode n1, TNode n2) {
- return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2);
+ return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2);
}
// congrence matching term helper
// we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs
// b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof,
// and use it to determine which option we need.
- if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) {
+ if(n2.getKind() == kind::EQUAL) {
if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) {
// We are in a sequence of identical equalities
} else {
// We have a "next node". Use it to guide us.
- Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL ||
- nodeAfterEqualitySequence.getKind() == kind::IFF);
+ Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL);
if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) {
Debug("pf::uf") << "\ndoing trans proof, got n2 " << n2 << "\n";
if(tb == 1) {
Debug("pf::uf") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n";
- Debug("pf::uf") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n";
+ Debug("pf::uf") << (n2.getKind() == kind::EQUAL) << "\n";
if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) {
Debug("pf::uf") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n";
}
ss << "(trans _ _ _ _ ";
- if((n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) &&
- (n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF))
+ if(n2.getKind() == kind::EQUAL && n1.getKind() == kind::EQUAL)
// Both elements of the transitivity rule are equalities/iffs
{
if(n1[0] == n2[0]) {
Unreachable();
}
Debug("pf::uf") << "++ trans proof[" << i << "], now have " << n1 << std::endl;
- } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) {
+ } else if(n1.getKind() == kind::EQUAL) {
// n1 is an equality/iff, but n2 is a predicate
if(n1[0] == n2) {
- n1 = n1[1].iffNode(NodeManager::currentNM()->mkConst(true));
+ n1 = n1[1].eqNode(NodeManager::currentNM()->mkConst(true));
ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")";
} else if(n1[1] == n2) {
- n1 = n1[0].iffNode(NodeManager::currentNM()->mkConst(true));
+ n1 = n1[0].eqNode(NodeManager::currentNM()->mkConst(true));
ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")";
} else {
Unreachable();
}
- } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) {
+ } else if(n2.getKind() == kind::EQUAL) {
// n2 is an equality/iff, but n1 is a predicate
if(n2[0] == n1) {
- n1 = n2[1].iffNode(NodeManager::currentNM()->mkConst(true));
+ n1 = n2[1].eqNode(NodeManager::currentNM()->mkConst(true));
ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")";
} else if(n2[1] == n1) {
- n1 = n2[0].iffNode(NodeManager::currentNM()->mkConst(true));
+ n1 = n2[0].eqNode(NodeManager::currentNM()->mkConst(true));
ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")";
} else {
Unreachable();
os << term;
return;
}
+ if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
+ os << "(p_app " << term << ")";
+ return;
+ }
Assert (term.getKind() == kind::APPLY_UF);
d_proofEngine->treatBoolsAsFormulas(false);
bool preRegister = false;
// Is this a variable add it to the list
- if (node.isVar()) {
+ if (node.isVar() && node.getKind()!=BOOLEAN_TERM_VARIABLE) {
d_booleanVariables.push_back(node);
} else {
theoryLiteral = true;
SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
Assert(!hasLiteral(iffNode), "Atom already mapped!");
- Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!");
+ Assert(iffNode.getKind() == EQUAL, "Expecting an EQUAL expression!");
Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
Debug("cnf") << "handleIff(" << iffNode << ")" << endl;
case ITE:
nodeLit = handleIte(node);
break;
- case IFF:
- nodeLit = handleIff(node);
- break;
case IMPLIES:
nodeLit = handleImplies(node);
break;
break;
case EQUAL:
if(node[0].getType().isBoolean()) {
- // normally this is an IFF, but EQUAL is possible with pseudobooleans
- nodeLit = handleIff(node[0].iffNode(node[1]));
+ nodeLit = handleIff(node);
} else {
nodeLit = convertAtom(node);
}
case OR:
convertAndAssertOr(node, negated);
break;
- case IFF:
- convertAndAssertIff(node, negated);
- break;
case XOR:
convertAndAssertXor(node, negated);
break;
case NOT:
convertAndAssert(node[0], !negated);
break;
+ case EQUAL:
+ if( node[0].getType().isBoolean() ){
+ convertAndAssertIff(node, negated);
+ break;
+ }
default:
{
Node nnode = node;
namespace CVC4 {
namespace smt {
-BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) :
- d_smt(smt),
- d_ff(),
- d_tt(),
- d_ffDt(),
- d_ttDt(),
- d_varCache(smt.d_userContext),
- d_termCache(smt.d_userContext),
- d_typeCache(),
- d_datatypeCache(),
- d_datatypeReverseCache() {
-
- // set up our "false" and "true" conversions based on command-line option
- if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS ||
- options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_NATIVE) {
- d_ff = NodeManager::currentNM()->mkConst(BitVector(1u, 0u));
- d_tt = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
- }
- if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS) {
- d_ffDt = d_ff;
- d_ttDt = d_tt;
- } else {
- Datatype spec("BooleanTerm");
- // don't change the order; false is assumed to come first by the model postprocessor
- spec.addConstructor(DatatypeConstructor("BT_False"));
- spec.addConstructor(DatatypeConstructor("BT_True"));
- const Datatype& dt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(spec).getDatatype();
- d_ffDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_False"].getConstructor()));
- d_ttDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_True"].getConstructor()));
- // mark this datatype type as being special for Boolean term conversion
- TypeNode::fromType(dt.getDatatypeType()).setAttribute(BooleanTermAttr(), Node::null());
- if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_DATATYPES) {
- Assert(d_ff.isNull() && d_tt.isNull());
- d_ff = d_ffDt;
- d_tt = d_ttDt;
- }
- }
-
- // assert that we set it up correctly
- Assert(!d_ff.isNull() && !d_tt.isNull());
- Assert(!d_ffDt.isNull() && !d_ttDt.isNull());
- Assert(d_ff != d_tt);
- Assert(d_ff.getType() == d_tt.getType());
- Assert(d_ffDt != d_ttDt);
- Assert(d_ffDt.getType() == d_ttDt.getType());
-
-}/* BooleanTermConverter::BooleanTermConverter() */
-
-static inline bool isBoolean(TNode top, unsigned i) {
- switch(top.getKind()) {
- case kind::NOT:
- case kind::AND:
- case kind::IFF:
- case kind::IMPLIES:
- case kind::OR:
- case kind::XOR:
- case kind::FORALL:
- case kind::EXISTS:
- case kind::REWRITE_RULE:
- case kind::RR_REWRITE:
- case kind::RR_DEDUCTION:
- case kind::RR_REDUCTION:
- case kind::INST_PATTERN:
- return true;
-
- case kind::ITE:
- if(i == 0) {
- return true;
- }
- return top.getType().isBoolean();
-
- default:
- return false;
- }
-}
-
-// This function rewrites "in" as an "as"---this is actually expected
-// to be for model-substitution, so the "in" is a Boolean-term-converted
-// node, and "as" is the original. See how it's used in function
-// handling, below.
-//
-// Note this isn't the case any longer, and parts of what's below have
-// been repurposed for *forward* conversion, meaning this works in either
-// direction.
-Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, bool >& processing) throw() {
- Debug("boolean-terms2") << "Rewrite as " << in << " " << as << std::endl;
- if(in.getType() == as) {
- return in;
- }
- if(in.getType().isBoolean()) {
- Assert(d_tt.getType() == as);
- return NodeManager::currentNM()->mkNode(kind::ITE, in, d_tt, d_ff);
- }
- if(as.isBoolean() && in.getType().isBitVector() && in.getType().getBitVectorSize() == 1) {
- return NodeManager::currentNM()->mkNode(kind::EQUAL, NodeManager::currentNM()->mkConst(BitVector(1u, 1u)), in);
- }
- TypeNode in_t = in.getType();
- if( processing.find( in_t )==processing.end() ){
- processing[in_t] = true;
- if(in.getType().isParametricDatatype() &&
- in.getType().isInstantiatedDatatype()) {
- // We have something here like (Pair Bool Bool)---need to dig inside
- // and make it (Pair BV1 BV1)
- Assert(as.isParametricDatatype() && as.isInstantiatedDatatype());
- const Datatype* dt2 = &as[0].getDatatype();
- std::vector<TypeNode> fromParams, toParams;
- for(unsigned i = 0; i < dt2->getNumParameters(); ++i) {
- fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
- toParams.push_back(as[i + 1]);
- }
- const Datatype* dt1;
- if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
- dt1 = d_datatypeCache[dt2];
- } else {
- dt1 = d_datatypeReverseCache[dt2];
- }
- Assert(dt1 != NULL, "expected datatype in cache");
- Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes");
- Node out;
- for(size_t i = 0; i < dt1->getNumConstructors(); ++i) {
- DatatypeConstructor ctor = (*dt1)[i];
- NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
- appctorb << (*dt2)[i].getConstructor();
- for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
- TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType());
- asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
- appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType, processing);
- }
- Node appctor = appctorb;
- if(i == 0) {
- out = appctor;
- } else {
- Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out);
- out = newOut;
- }
- }
- processing.erase( in_t );
- return out;
- }
- if(in.getType().isDatatype()) {
- if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
- processing.erase( in_t );
- return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in);
- }
- Assert(as.isDatatype());
- const Datatype* dt2 = &as.getDatatype();
- const Datatype* dt1;
- if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
- dt1 = d_datatypeCache[dt2];
- } else {
- dt1 = d_datatypeReverseCache[dt2];
- }
- Assert(dt1 != NULL, "expected datatype in cache");
- Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes");
- Node out;
- for(size_t i = 0; i < dt1->getNumConstructors(); ++i) {
- DatatypeConstructor ctor = (*dt1)[i];
- NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
- appctorb << (*dt2)[i].getConstructor();
- for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
- appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()), processing);
- }
- Node appctor = appctorb;
- if(i == 0) {
- out = appctor;
- } else {
- Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out);
- out = newOut;
- }
- }
- processing.erase( in_t );
- return out;
- }
- if(in.getType().isArray()) {
- // convert in to in'
- // e.g. in : (Array Int Bool)
- // for in' : (Array Int (_ BitVec 1))
- // then subs in |=> \array_lambda ( \lambda (x:Int) . [convert (read a' x) x]
- Assert(as.isArray());
- Assert(as.getArrayIndexType() == in.getType().getArrayIndexType());
- Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType());
- Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType());
- Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x);
- Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x);
- Node selprime = rewriteAs(sel, as.getArrayConstituentType(), processing);
- Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime);
- Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam);
- Assert(out.getType() == as);
- processing.erase( in_t );
- return out;
- }
- Unhandled(in);
- }else{
- Message() << "Type " << in_t << " involving Boolean sort is not supported." << std::endl;
- exit( 0 );
- }
-}
-
-const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw() {
- const Datatype*& out = d_datatypeCache[&dt];
- if(out != NULL) {
- return *out;
- }
-
- Debug("boolean-terms") << "convertDatatype: considering " << dt.getName() << endl;
- for(Datatype::const_iterator c = dt.begin(); c != dt.end(); ++c) {
- TypeNode t = TypeNode::fromType((*c).getConstructor().getType());
- for(TypeNode::const_iterator a = t.begin(); a != t.end(); ++a) {
- TypeNode converted = convertType(*a, true);
- Debug("boolean-terms") << "GOT: " << converted << ":" << converted.getId() << endl;
- if(*a != converted) {
- SortConstructorType mySelfType;
- set<Type> unresolvedTypes;
- if(dt.isParametric()) {
- mySelfType = NodeManager::currentNM()->toExprManager()->mkSortConstructor(dt.getName() + "'", dt.getNumParameters());
- unresolvedTypes.insert(mySelfType);
- }
- vector<Datatype> newDtVector;
- if(dt.isParametric()) {
- newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters(), false));
- } else {
- newDtVector.push_back(Datatype(dt.getName() + "'", false));
- }
- Datatype& newDt = newDtVector.front();
- Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl;
- for(c = dt.begin(); c != dt.end(); ++c) {
- DatatypeConstructor ctor((*c).getName() + "'", (*c).getTesterName() + "'");
- t = TypeNode::fromType((*c).getConstructor().getType());
- for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
- Type argType = (*a).getType().getRangeType();
- if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) {
- Debug("boolean-terms") << "argtype " << argType << " is self" << endl;
- if(dt.isParametric()) {
- Debug("boolean-terms") << "is-parametric self is " << mySelfType << endl;
- ctor.addArg((*a).getName() + "'", mySelfType.instantiate(DatatypeType(argType).getDatatype().getParameters()));
- } else {
- ctor.addArg((*a).getName() + "'", DatatypeSelfType());
- }
- } else {
- Debug("boolean-terms") << "argtype " << argType << " is NOT self" << endl;
- converted = convertType(TypeNode::fromType(argType), true);
- if(TypeNode::fromType(argType) != converted) {
- ctor.addArg((*a).getName() + "'", converted.toType());
- } else {
- ctor.addArg((*a).getName() + "'", argType);
- }
- }
- }
- newDt.addConstructor(ctor);
- }
- vector<DatatypeType> newDttVector =
- NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes);
- DatatypeType& newDtt = newDttVector.front();
- const Datatype& newD = newDtt.getDatatype();
- for(c = dt.begin(); c != dt.end(); ++c) {
- Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl;
- const DatatypeConstructor *newC;
- Node::fromExpr((*(newC = &newD[(*c).getName() + "'"])).getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr?
- Debug("boolean-terms") << "mapped " << newD[(*c).getName() + "'"].getConstructor() << " to " << (*c).getConstructor() << endl;
- d_varCache[Node::fromExpr((*c).getConstructor())] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
- d_varCache[Node::fromExpr((*c).getTester())] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
- for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
- Node::fromExpr((*newC)[(*a).getName() + "'"].getSelector()).setAttribute(BooleanTermAttr(), Node::fromExpr((*a).getSelector()));// other attr?
- d_varCache[Node::fromExpr((*a).getSelector())] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
- }
- }
- out = &newD;
- d_datatypeReverseCache[&newD] = &dt;
- return newD;
- }
- }
- }
-
- // this is identity; don't need the reverse cache
- out = &dt;
- return dt;
-
-}/* BooleanTermConverter::convertDatatype() */
-
-TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext) {
- Debug("boolean-terms") << "CONVERT-TYPE[" << type << ":" << type.getId() << ", " << datatypesContext << "]" << endl;
- // This function recursively converts the type.
- if(type.isBoolean()) {
- return datatypesContext ? d_ttDt.getType() : d_tt.getType();
- }
- const pair<TypeNode, bool> cacheKey(type, datatypesContext);
- if(d_typeCache.find(cacheKey) != d_typeCache.end()) {
- TypeNode out = d_typeCache[cacheKey];
- return out.isNull() ? type : out;
- }
- TypeNode& outNode = d_typeCache[cacheKey];
- if(type.getKind() == kind::DATATYPE_TYPE ||
- type.getKind() == kind::PARAMETRIC_DATATYPE) {
- bool parametric = (type.getKind() == kind::PARAMETRIC_DATATYPE);
- const Datatype& dt = parametric ? type[0].getDatatype() : type.getDatatype();
- TypeNode out = TypeNode::fromType(convertDatatype(dt).getDatatypeType());
- Debug("boolean-terms") << "AFTER, got "<< out << " param:" << parametric << endl;
- if(parametric) {
- // re-parameterize the translation
- vector<TypeNode> params = type.getParamTypes();
- for(size_t i = 0; i < params.size(); ++i) {
- Debug("boolean-terms") << "in loop, got "<< params[i] << endl;
- params[i] = convertType(params[i], true);
- Debug("boolean-terms") << "in loop, convert to "<< params[i] << endl;
- }
- params.insert(params.begin(), out[0]);
- out = NodeManager::currentNM()->mkTypeNode(kind::PARAMETRIC_DATATYPE, params);
- Debug("boolean-terms") << "got OUT: " << out << endl;
- }
- if(out != type) {
- outNode = out;// cache it
- Debug("boolean-terms") << "OUT is same as TYPE" << endl;
- } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl;
- return out;
- }
- if(!type.isSort() && type.getNumChildren() > 0) {
- Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl;
- // This should handle tuples and arrays ok.
- // Might handle function types too, but they can't go
- // in other types, so it doesn't matter.
- NodeBuilder<> b(type.getKind());
- if(type.getMetaKind() == kind::metakind::PARAMETERIZED) {
- b << type.getOperator();
- }
- for(TypeNode::iterator i = type.begin(); i != type.end(); ++i) {
- b << convertType(*i, false);
- }
- TypeNode out = b;
- if(out != type) {
- outNode = out;// cache it
- }
- Debug("boolean-terms") << "here at B, returning " << out << ":" << out.getId() << endl;
- return out;
- }
- // leave the cache at Null
- return type;
-}/* BooleanTermConverter::convertType() */
-
-// look for vars from "vars" that occur in a term-context in n; transfer them to output.
-static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TNode>& output, bool boolParent, std::hash_set< std::pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> >& alreadySeen) {
- if(vars.empty()) {
- return;
- }
- const pair<TNode, bool> cacheKey(n, boolParent);
- if(alreadySeen.find(cacheKey) != alreadySeen.end()) {
- return;
- }
- alreadySeen.insert(cacheKey);
-
- if(n.isVar() && vars.find(n) != vars.end() && !boolParent) {
- vars.erase(n);
- output.insert(n);
- if(vars.empty()) {
- return;
- }
- }
- for(size_t i = 0; i < n.getNumChildren(); ++i) {
- collectVarsInTermContext(n[i], vars, output, isBoolean(n, i), alreadySeen);
- if(vars.empty()) {
- return;
- }
- }
-}
-
-Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw() {
-
- stack< triple<TNode, theory::TheoryId, bool> > worklist;
- worklist.push(triple<TNode, theory::TheoryId, bool>(top, parentTheory, false));
- stack< NodeBuilder<> > result;
- //AJR: not sure what the significance of "TUPLE" is here, seems to be a placeholder. Since TUPLE is no longer a kind, replacing this with "AND".
- //result.push(NodeBuilder<>(kind::TUPLE));
- result.push(NodeBuilder<>(kind::AND));
-
- NodeManager* nm = NodeManager::currentNM();
-
- while(!worklist.empty()) {
- top = worklist.top().first;
- parentTheory = worklist.top().second;
- bool& childrenPushed = worklist.top().third;
-
- Kind k = top.getKind();
- kind::MetaKind mk = top.getMetaKind();
-
- // we only distinguish between datatypes, booleans, and "other", and we
- // don't even distinguish datatypes except when in "native" conversion
- // mode
- if(parentTheory != theory::THEORY_BOOL) {
- if(options::booleanTermConversionMode() != BOOLEAN_TERM_CONVERT_NATIVE ||
- parentTheory != theory::THEORY_DATATYPES) {
- parentTheory = theory::THEORY_BUILTIN;
- }
- }
-
- if(!childrenPushed) {
- Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl;
-
- BooleanTermVarCache::iterator i = d_varCache.find(top);
- if(i != d_varCache.end()) {
- result.top() << ((*i).second.isNull() ? Node(top) : (*i).second);
- worklist.pop();
- goto next_worklist;
- }
- BooleanTermCache::iterator j = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory));
- if(j != d_termCache.end()) {
- result.top() << ((*j).second.isNull() ? Node(top) : (*j).second);
- worklist.pop();
- goto next_worklist;
- }
-
- if(quantBoolVars.find(top) != quantBoolVars.end()) {
- // this Bool variable is quantified over and we're changing it to a BitVector var
- if(parentTheory == theory::THEORY_BOOL) {
- result.top() << quantBoolVars[top].eqNode(d_tt);
- } else {
- result.top() << quantBoolVars[top];
- }
- worklist.pop();
- goto next_worklist;
- }
-
- if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean() && top.getKind()!=kind::SEP_STAR && top.getKind()!=kind::SEP_WAND) {
- // still need to rewrite e.g. function applications over boolean
- Node topRewritten = rewriteBooleanTermsRec(top, theory::THEORY_BOOL, quantBoolVars);
- Node n;
- if(parentTheory == theory::THEORY_DATATYPES) {
- n = nm->mkNode(kind::ITE, topRewritten, d_ttDt, d_ffDt);
- } else {
- n = nm->mkNode(kind::ITE, topRewritten, d_tt, d_ff);
- }
- Debug("boolean-terms") << "constructed ITE: " << n << endl;
- result.top() << n;
- worklist.pop();
- goto next_worklist;
- }
-
- if(mk == kind::metakind::CONSTANT) {
- if(k == kind::STORE_ALL) {
- const ArrayStoreAll& asa = top.getConst<ArrayStoreAll>();
- ArrayType arrType = asa.getType();
- TypeNode indexType = TypeNode::fromType(arrType.getIndexType());
- Type constituentType = arrType.getConstituentType();
- if(constituentType.isBoolean()) {
- // we have store_all(true) or store_all(false)
- // just turn it into store_all(1) or store_all(0)
- if(indexType.isBoolean()) {
- // change index type to BV(1) also
- indexType = d_tt.getType();
- }
- ArrayStoreAll asaRepl(nm->mkArrayType(indexType, d_tt.getType()).toType(),
- (asa.getExpr().getConst<bool>() ? d_tt : d_ff).toExpr());
- Node n = nm->mkConst(asaRepl);
- Debug("boolean-terms") << " returning new store_all: " << n << endl;
- result.top() << n;
- worklist.pop();
- goto next_worklist;
- }
- if(indexType.isBoolean()) {
- // must change index type to BV(1)
- indexType = d_tt.getType();
- ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr());
- Node n = nm->mkConst(asaRepl);
- Debug("boolean-terms") << " returning new store_all: " << n << endl;
- result.top() << n;
- worklist.pop();
- goto next_worklist;
- }
- }
- result.top() << top;
- worklist.pop();
- goto next_worklist;
- } else if(mk == kind::metakind::VARIABLE) {
- TypeNode t = top.getType();
- if(t.isFunction()) {
- for(unsigned i = 0; i < t.getNumChildren(); ++i) {
- TypeNode newType = convertType(t[i], false);
- // is this the return type? (allowed to be Bool)
- bool returnType = (i == t.getNumChildren() - 1);
- if(newType != t[i] && (!t[i].isBoolean() || !returnType)) {
- vector<TypeNode> argTypes = t.getArgTypes();
- for(unsigned j = 0; j < argTypes.size(); ++j) {
- argTypes[j] = convertType(argTypes[j], false);
- }
- TypeNode rangeType = t.getRangeType();
- if(!rangeType.isBoolean()) {
- rangeType = convertType(rangeType, false);
- }
- TypeNode newType = nm->mkFunctionType(argTypes, rangeType);
- Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__",
- newType, "a function introduced by Boolean-term conversion",
- NodeManager::SKOLEM_EXACT_NAME);
- Debug("boolean-terms") << "constructed func: " << n << " of type " << newType << endl;
- top.setAttribute(BooleanTermAttr(), n);
- NodeBuilder<> boundVarsBuilder(kind::BOUND_VAR_LIST);
- NodeBuilder<> bodyBuilder(kind::APPLY_UF);
- bodyBuilder << n;
- for(unsigned j = 0; j < t.getNumChildren() - 1; ++j) {
- Node var = nm->mkBoundVar(t[j]);
- boundVarsBuilder << var;
- if(t[j] != argTypes[j]) {
- std::map< TypeNode, bool > processing;
- bodyBuilder << rewriteAs(var, argTypes[j], processing);
- } else {
- bodyBuilder << var;
- }
- }
- Node boundVars = boundVarsBuilder;
- Node body = bodyBuilder;
- if(t.getRangeType() != rangeType) {
- std::map< TypeNode, bool > processing;
- Node convbody = rewriteAs(body, t.getRangeType(), processing);
- body = convbody;
- }
- Node lam = nm->mkNode(kind::LAMBDA, boundVars, body);
- Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl;
- d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam);
- d_varCache[top] = n;
- result.top() << n;
- worklist.pop();
- goto next_worklist;
- }
- }
- } else if(t.isArray()) {
- TypeNode indexType = convertType(t.getArrayIndexType(), false);
- TypeNode constituentType = convertType(t.getArrayConstituentType(), false);
- if(indexType != t.getArrayIndexType() && constituentType == t.getArrayConstituentType()) {
- TypeNode newType = nm->mkArrayType(indexType, constituentType);
- Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
- newType, "an array variable introduced by Boolean-term conversion",
- NodeManager::SKOLEM_EXACT_NAME);
- top.setAttribute(BooleanTermAttr(), n);
- Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
- Node n_ff = nm->mkNode(kind::SELECT, n, d_ff);
- Node n_tt = nm->mkNode(kind::SELECT, n, d_tt);
- Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), (*TypeEnumerator(n_ff.getType())).toExpr()));
- Node repl = nm->mkNode(kind::STORE,
- nm->mkNode(kind::STORE, base, nm->mkConst(true),
- n_tt),
- nm->mkConst(false), n_ff);
- Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
- d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
- d_varCache[top] = n;
- result.top() << n;
- worklist.pop();
- goto next_worklist;
- } else if(indexType == t.getArrayIndexType() && constituentType != t.getArrayConstituentType()) {
- TypeNode newType = nm->mkArrayType(indexType, constituentType);
- Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
- newType, "an array variable introduced by Boolean-term conversion",
- NodeManager::SKOLEM_EXACT_NAME);
- top.setAttribute(BooleanTermAttr(), n);
- Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
- d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
- d_varCache[top] = n;
- result.top() << n;
- worklist.pop();
- goto next_worklist;
- } else if(indexType != t.getArrayIndexType() && constituentType != t.getArrayConstituentType()) {
- TypeNode newType = nm->mkArrayType(indexType, constituentType);
- Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
- newType, "an array variable introduced by Boolean-term conversion",
- NodeManager::SKOLEM_EXACT_NAME);
- top.setAttribute(BooleanTermAttr(), n);
- Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
- Node n_ff = nm->mkNode(kind::SELECT, n, d_ff);
- Node n_tt = nm->mkNode(kind::SELECT, n, d_tt);
- Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), nm->mkConst(false).toExpr()));
- Node repl = nm->mkNode(kind::STORE,
- nm->mkNode(kind::STORE, base, nm->mkConst(false),
- nm->mkNode(kind::EQUAL, n_ff, d_tt)), nm->mkConst(true),
- nm->mkNode(kind::EQUAL, n_tt, d_tt));
- Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
- d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
- d_varCache[top] = n;
- result.top() << n;
- worklist.pop();
- goto next_worklist;
- }
- d_varCache[top] = Node::null();
- result.top() << top;
- worklist.pop();
- goto next_worklist;
- } else if(t.isDatatype() || t.isParametricDatatype()) {
- Debug("boolean-terms") << "found a var of datatype type" << endl;
- TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES);
- if(t != newT) {
- Assert(d_varCache.find(top) == d_varCache.end(),
- "Node `%s' already in cache ?!", top.toString().c_str());
- Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
- newT, "a datatype variable introduced by Boolean-term conversion",
- NodeManager::SKOLEM_EXACT_NAME);
- Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
- top.setAttribute(BooleanTermAttr(), n);
- d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
- Debug("boolean-terms") << "constructed: " << n << " of type " << newT << endl;
- d_varCache[top] = n;
- result.top() << n;
- worklist.pop();
- goto next_worklist;
- } else {
- d_varCache[top] = Node::null();
- result.top() << top;
- worklist.pop();
- goto next_worklist;
- }
- } else if(t.isConstructor()) {
- Assert(parentTheory != theory::THEORY_BOOL);
- Assert(t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ||
- t[t.getNumChildren() - 1].getKind() == kind::PARAMETRIC_DATATYPE);
- const Datatype& dt = t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ?
- t[t.getNumChildren() - 1].getDatatype() :
- t[t.getNumChildren() - 1][0].getDatatype();
- TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
- const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getDatatype();
- if(dt != dt2) {
- Assert(d_varCache.find(top) != d_varCache.end(),
- "constructor `%s' not in cache", top.toString().c_str());
- result.top() << d_varCache[top].get();
- worklist.pop();
- goto next_worklist;
- }
- d_varCache[top] = Node::null();
- result.top() << top;
- worklist.pop();
- goto next_worklist;
- } else if(t.isTester() || t.isSelector()) {
- Assert(parentTheory != theory::THEORY_BOOL);
- const Datatype& dt = t[0].getKind() == kind::DATATYPE_TYPE ?
- t[0].getDatatype() :
- t[0][0].getDatatype();
- TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
- const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getDatatype();
- if(dt != dt2) {
- Assert(d_varCache.find(top) != d_varCache.end(),
- "tester or selector `%s' not in cache", top.toString().c_str());
- result.top() << d_varCache[top].get();
- worklist.pop();
- goto next_worklist;
- } else {
- d_varCache[top] = Node::null();
- result.top() << top;
- worklist.pop();
- goto next_worklist;
- }
- } else if(!t.isSort() && t.getNumChildren() > 0) {
- if( t.getKind()!=kind::SEP_STAR && t.getKind()!=kind::SEP_WAND ){
- for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) {
- if((*i).isBoolean()) {
- vector<TypeNode> argTypes(t.begin(), t.end());
- replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType());
- TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes);
- Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
- newType, "a variable introduced by Boolean-term conversion",
- NodeManager::SKOLEM_EXACT_NAME);
- Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
- top.setAttribute(BooleanTermAttr(), n);
- d_varCache[top] = n;
- result.top() << n;
- worklist.pop();
- goto next_worklist;
- }
- }
- }
- }
- result.top() << top;
- worklist.pop();
- goto next_worklist;
- }
- switch(k) {
- //case kind::INST_ATTRIBUTE:
- case kind::BOUND_VAR_LIST:
- result.top() << top;
- worklist.pop();
- goto next_worklist;
-
- case kind::REWRITE_RULE:
- case kind::RR_REWRITE:
- case kind::RR_DEDUCTION:
- case kind::RR_REDUCTION:
- case kind::SEP_STAR:
- case kind::SEP_WAND:
- // not yet supported
- result.top() << top;
- worklist.pop();
- goto next_worklist;
-
- case kind::FORALL:
- case kind::EXISTS: {
- Debug("bt") << "looking at quantifier -> " << top << endl;
- set<TNode> ourVars;
- set<TNode> output;
- for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) {
- if((*i).getType().isBoolean()) {
- ourVars.insert(*i);
- } else if(convertType((*i).getType(), false) != (*i).getType()) {
- output.insert(*i);
- }
- }
- if(ourVars.empty() && output.empty()) {
- // Simple case, quantifier doesn't quantify over Boolean vars,
- // no special handling needed for quantifier. Fall through.
- Debug("bt") << "- quantifier simple case (1), no Boolean vars bound" << endl;
- } else {
- hash_set< pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> > alreadySeen;
- collectVarsInTermContext(top[1], ourVars, output, true, alreadySeen);
- if(output.empty()) {
- // Simple case, quantifier quantifies over Boolean vars, but they
- // don't occur in term context. Fall through.
- Debug("bt") << "- quantifier simple case (2), Boolean vars bound but not used in term context" << endl;
- } else {
- Debug("bt") << "- quantifier case (3), Boolean vars bound and used in term context" << endl;
- // We have Boolean vars appearing in term context. Convert their
- // types in the quantifier.
- for(set<TNode>::const_iterator i = output.begin(); i != output.end(); ++i) {
- Node newVar = nm->mkBoundVar((*i).toString(), convertType((*i).getType(), false));
- Assert(quantBoolVars.find(*i) == quantBoolVars.end(), "bad quantifier: shares a bound var with another quantifier (don't do that!)");
- quantBoolVars[*i] = newVar;
- }
- vector<TNode> boundVars;
- for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) {
- map<TNode, Node>::const_iterator j = quantBoolVars.find(*i);
- if(j == quantBoolVars.end()) {
- boundVars.push_back(*i);
- } else {
- boundVars.push_back((*j).second);
- }
- }
- Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars);
- Node body = rewriteBooleanTermsRec(top[1], theory::THEORY_BOOL, quantBoolVars);
- Node quant;
- if( top.getNumChildren()==3 ){
- Node ipl = rewriteBooleanTermsRec(top[2], theory::THEORY_BOOL, quantBoolVars);
- quant = nm->mkNode(top.getKind(), boundVarList, body, ipl );
- }else{
- quant = nm->mkNode(top.getKind(), boundVarList, body);
- }
- Debug("bt") << "rewrote quantifier to -> " << quant << endl;
- d_termCache[make_pair(top, theory::THEORY_BOOL)] = quant;
- d_termCache[make_pair(top, theory::THEORY_BUILTIN)] = quant.iteNode(d_tt, d_ff);
- d_termCache[make_pair(top, theory::THEORY_DATATYPES)] = quant.iteNode(d_tt, d_ff);
- result.top() << quant;
- worklist.pop();
- goto next_worklist;
- }
- }
- /* intentional fall-through for some cases above */
- }
-
- default:
- result.push(NodeBuilder<>(k));
- Debug("bt") << "looking at: " << top << endl;
- // rewrite the operator, as necessary
- if(mk == kind::metakind::PARAMETERIZED) {
- if(k == kind::APPLY_TYPE_ASCRIPTION) {
- Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType()));
- result.top() << asc;
- Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl;
- asc.setAttribute(BooleanTermAttr(), top.getOperator());
- } else if(kindToTheoryId(k) != THEORY_BV &&
- k != kind::TUPLE_UPDATE &&
- k != kind::RECORD_UPDATE &&
- k != kind::DIVISIBLE &&
- // Theory parametric functions go here
- k != kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR &&
- k != kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT &&
- k != kind::FLOATINGPOINT_TO_FP_REAL &&
- k != kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR &&
- k != kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR &&
- k != kind::FLOATINGPOINT_TO_UBV &&
- k != kind::FLOATINGPOINT_TO_SBV &&
- k != kind::FLOATINGPOINT_TO_REAL
- ) {
- Debug("bt") << "rewriting: " << top.getOperator() << endl;
- result.top() << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars);
- Debug("bt") << "got: " << result.top().getOperator() << endl;
- } else {
- result.top() << top.getOperator();
- }
- }
- // push children
- for(int i = top.getNumChildren() - 1; i >= 0; --i) {
- Debug("bt") << "rewriting: " << top[i] << endl;
- worklist.push(triple<TNode, theory::TheoryId, bool>(top[i], top.getKind() == kind::CHAIN ? parentTheory : ((isBoolean(top, i) || top.getKind()==kind::INST_ATTRIBUTE) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN)), false));
- //b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? , quantBoolVars);
- //Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl;
- }
- childrenPushed = true;
- }
- } else {
- Node n = result.top();
- result.pop();
- Debug("boolean-terms") << "constructed: " << n << " of type " << n.getType() << endl;
- if(parentTheory == theory::THEORY_BOOL) {
- if(n.getType().isBitVector() &&
- n.getType().getBitVectorSize() == 1) {
- n = nm->mkNode(kind::EQUAL, n, d_tt);
- } else if(n.getType().isDatatype() &&
- n.getType().hasAttribute(BooleanTermAttr())) {
- n = nm->mkNode(kind::EQUAL, n, d_ttDt);
- }
- }
- d_termCache[make_pair(top, parentTheory)] = n;
- result.top() << n;
- worklist.pop();
- goto next_worklist;
- }
-
- next_worklist:
- ;
- }
-
- Assert(worklist.size() == 0);
- Assert(result.size() == 1);
- Node retval = result.top()[0];
- result.top().clear();
- result.pop();
- return retval;
-
-}/* BooleanTermConverter::rewriteBooleanTermsRec() */
-
}/* CVC4::smt namespace */
}/* CVC4 namespace */
namespace CVC4 {
namespace smt {
-namespace attr {
- struct BooleanTermAttrTag { };
-}/* CVC4::smt::attr namespace */
-
-typedef expr::Attribute<attr::BooleanTermAttrTag, Node> BooleanTermAttr;
-
-class BooleanTermConverter {
- /** The type of the Boolean term conversion variable cache */
- typedef context::CDHashMap<Node, Node, NodeHashFunction> BooleanTermVarCache;
-
- /** The type of the Boolean term conversion cache */
- typedef context::CDHashMap< std::pair<Node, theory::TheoryId>, Node,
- PairHashFunction< Node, bool,
- NodeHashFunction, std::hash<size_t> > > BooleanTermCache;
- /** The type of the Boolean term conversion type cache */
- typedef std::hash_map< std::pair<TypeNode, bool>, TypeNode,
- PairHashFunction< TypeNode, bool,
- TypeNodeHashFunction, std::hash<int> > > BooleanTermTypeCache;
- /** The type of the Boolean term conversion datatype cache */
- typedef std::hash_map<const Datatype*, const Datatype*, DatatypeHashFunction> BooleanTermDatatypeCache;
-
- /** The SmtEngine to which we're associated */
- SmtEngine& d_smt;
-
- /** The conversion for "false." */
- Node d_ff;
- /** The conversion for "true." */
- Node d_tt;
- /** The conversion for "false" when in datatypes contexts. */
- Node d_ffDt;
- /** The conversion for "true" when in datatypes contexts. */
- Node d_ttDt;
-
- /** The cache used during Boolean term variable conversion */
- BooleanTermVarCache d_varCache;
- /** The cache used during Boolean term conversion */
- BooleanTermCache d_termCache;
- /** The cache used during Boolean term type conversion */
- BooleanTermTypeCache d_typeCache;
- /** The cache used during Boolean term datatype conversion */
- BooleanTermDatatypeCache d_datatypeCache;
- /** A (reverse) cache for Boolean term datatype conversion */
- BooleanTermDatatypeCache d_datatypeReverseCache;
-
- Node rewriteAs(TNode in, TypeNode as, std::map< TypeNode, bool >& processing) throw();
-
- /**
- * Scan a datatype for and convert as necessary.
- */
- const Datatype& convertDatatype(const Datatype& dt) throw();
-
- /**
- * Convert a type.
- */
- TypeNode convertType(TypeNode type, bool datatypesContext);
-
- Node rewriteBooleanTermsRec(TNode n, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw();
-
-public:
-
- /**
- * Construct a Boolean-term converter associated to the given
- * SmtEngine.
- */
- BooleanTermConverter(SmtEngine& smt);
-
- /**
- * Rewrite Boolean terms under a node. The node itself is not converted
- * if boolParent is true, but its Boolean subterms appearing in a
- * non-Boolean context will be rewritten.
- */
- Node rewriteBooleanTerms(TNode n, bool boolParent = true, bool dtParent = false) throw() {
- std::map<TNode, Node> quantBoolVars;
- Assert(!(boolParent && dtParent));
- return rewriteBooleanTermsRec(n, boolParent ? theory::THEORY_BOOL : (dtParent ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), quantBoolVars);
- }
-
-};/* class BooleanTermConverter */
-
}/* CVC4::smt namespace */
}/* CVC4 namespace */
namespace CVC4 {
-RemoveITE::RemoveITE(context::UserContext* u)
+RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u)
: d_iteCache(u)
{
d_containsVisitor = new theory::ContainsTermITEVisitor();
}
-RemoveITE::~RemoveITE(){
+RemoveTermFormulas::~RemoveTermFormulas(){
delete d_containsVisitor;
}
-void RemoveITE::garbageCollect(){
+void RemoveTermFormulas::garbageCollect(){
d_containsVisitor->garbageCollect();
}
-theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() {
+theory::ContainsTermITEVisitor* RemoveTermFormulas::getContainsVisitor() {
return d_containsVisitor;
}
-size_t RemoveITE::collectedCacheSizes() const{
+size_t RemoveTermFormulas::collectedCacheSizes() const{
return d_containsVisitor->cache_size() + d_iteCache.size();
}
-void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
+void RemoveTermFormulas::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
{
size_t n = output.size();
for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
// Do this in two steps to avoid Node problems(?)
// Appears related to bug 512, splitting this into two lines
// fixes the bug on clang on Mac OS
- Node itesRemoved = run(output[i], output, iteSkolemMap, false);
+ Node itesRemoved = run(output[i], output, iteSkolemMap, false, false);
// In some calling contexts, not necessary to report dependence information.
if (reportDeps &&
(options::unsatCores() || options::fewerPreprocessingHoles())) {
}
}
-bool RemoveITE::containsTermITE(TNode e) const {
+bool RemoveTermFormulas::containsTermITE(TNode e) const {
return d_containsVisitor->containsTermITE(e);
}
-Node RemoveITE::run(TNode node, std::vector<Node>& output,
- IteSkolemMap& iteSkolemMap, bool inQuant) {
+Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
+ IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm) {
// Current node
- Debug("ite") << "removeITEs(" << node << ")" << endl;
-
- if(node.isVar() || node.isConst() ||
- (options::biasedITERemoval() && !containsTermITE(node))){
+ Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << endl;
+
+ //if(node.isVar() || node.isConst()){
+ // (options::biasedITERemoval() && !containsTermITE(node))){
+ //if(node.isVar()){
+ // return Node(node);
+ //}
+ if( node.getKind()==kind::INST_PATTERN_LIST ){
return Node(node);
}
// The result may be cached already
- std::pair<Node, bool> cacheKey(node, inQuant);
+ int cv = cacheVal( inQuant, inTerm );
+ std::pair<Node, int> cacheKey(node, cv);
NodeManager *nodeManager = NodeManager::currentNM();
ITECache::const_iterator i = d_iteCache.find(cacheKey);
if(i != d_iteCache.end()) {
return cached.isNull() ? Node(node) : cached;
}
- // Remember that we're inside a quantifier
- if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
- inQuant = true;
- }
- // If an ITE replace it
+ // If an ITE, replace it
+ TypeNode nodeType = node.getType();
if(node.getKind() == kind::ITE) {
- TypeNode nodeType = node.getType();
if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
Node skolem;
// Make the skolem to represent the ITE
d_iteCache.insert(cacheKey, skolem);
// Remove ITEs from the new assertion, rewrite it and push it to the output
- newAssertion = run(newAssertion, output, iteSkolemMap, inQuant);
+ newAssertion = run(newAssertion, output, iteSkolemMap, false, false);
iteSkolemMap[skolem] = output.size();
output.push_back(newAssertion);
return skolem;
}
}
+ //if a non-variable Boolean term, replace it
+ if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){
+ Node skolem;
+ // Make the skolem to represent the Boolean term
+ //skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable introduced due to Boolean term removal");
+ skolem = nodeManager->mkBooleanTermVariable();
+
+ // The new assertion
+ Node newAssertion = skolem.eqNode( node );
+ Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
+
+ // Attach the skolem
+ d_iteCache.insert(cacheKey, skolem);
+
+ // Remove ITEs from the new assertion, rewrite it and push it to the output
+ newAssertion = run(newAssertion, output, iteSkolemMap, false, false);
+
+ iteSkolemMap[skolem] = output.size();
+ output.push_back(newAssertion);
+
+ // The representation is now the skolem
+ return skolem;
+ }
+
+ if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+ // Remember if we're inside a quantifier
+ inQuant = true;
+ }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL &&
+ node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR &&
+ node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL ){
+ // Remember if we're inside a term
+ Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl;
+ inTerm = true;
+ }
// If not an ITE, go deep
vector<Node> newChildren;
}
// Remove the ITEs from the children
for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
- Node newChild = run(*it, output, iteSkolemMap, inQuant);
+ Node newChild = run(*it, output, iteSkolemMap, inQuant, inTerm);
somethingChanged |= (newChild != *it);
newChildren.push_back(newChild);
}
}
}
-Node RemoveITE::replace(TNode node, bool inQuant) const {
- if(node.isVar() || node.isConst() ||
- (options::biasedITERemoval() && !containsTermITE(node))){
+Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const {
+ //if(node.isVar() || node.isConst()){
+ // (options::biasedITERemoval() && !containsTermITE(node))){
+ //if(node.isVar()){
+ // return Node(node);
+ //}
+ if( node.getKind()==kind::INST_PATTERN_LIST ){
return Node(node);
}
// Check the cache
NodeManager *nodeManager = NodeManager::currentNM();
- ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant));
+ int cv = cacheVal( inQuant, inTerm );
+ ITECache::const_iterator i = d_iteCache.find(make_pair(node, cv));
if(i != d_iteCache.end()) {
Node cached = (*i).second;
return cached.isNull() ? Node(node) : cached;
}
- // Remember that we're inside a quantifier
if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+ // Remember if we're inside a quantifier
inQuant = true;
- }
+ }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && node.getKind()!=kind::EQUAL ){
+ // Remember if we're inside a term
+ inTerm = true;
+ }
vector<Node> newChildren;
bool somethingChanged = false;
}
// Replace in children
for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
- Node newChild = replace(*it, inQuant);
+ Node newChild = replace(*it, inQuant, inTerm);
somethingChanged |= (newChild != *it);
newChildren.push_back(newChild);
}
typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
-class RemoveITE {
- typedef context::CDInsertHashMap< std::pair<Node, bool>, Node, PairHashFunction<Node, bool, NodeHashFunction, BoolHashFunction> > ITECache;
+class RemoveTermFormulas {
+ typedef context::CDInsertHashMap< std::pair<Node, int>, Node, PairHashFunction<Node, int, NodeHashFunction, BoolHashFunction> > ITECache;
ITECache d_iteCache;
-
+ static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); }
public:
- RemoveITE(context::UserContext* u);
- ~RemoveITE();
+ RemoveTermFormulas(context::UserContext* u);
+ ~RemoveTermFormulas();
/**
* Removes the ITE nodes by introducing skolem variables. All
* ite created in conjunction with that skolem variable.
*/
Node run(TNode node, std::vector<Node>& additionalAssertions,
- IteSkolemMap& iteSkolemMap, bool inQuant);
+ IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm);
/**
* Substitute under node using pre-existing cache. Do not remove
* any ITEs not seen during previous runs.
*/
- Node replace(TNode node, bool inQuant = false) const;
+ Node replace(TNode node, bool inQuant = false, bool inTerm = false) const;
/** Returns true if e contains a term ite. */
bool containsTermITE(TNode e) const;
/** Garbage collects non-context dependent data-structures. */
void garbageCollect();
- /** Return the RemoveITE's containsVisitor. */
+ /** Return the RemoveTermFormulas's containsVisitor. */
theory::ContainsTermITEVisitor* getContainsVisitor();
private:
namespace CVC4 {
namespace smt {
-Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
- if(n.getType().isSubtypeOf(asType)) {
- // good to go, we have the right type
- return n;
- }
- if(n.getKind() == kind::LAMBDA) {
- Assert(asType.isFunction());
- Node rhs = rewriteAs(n[1], asType[1]);
- Node out = NodeManager::currentNM()->mkNode(kind::LAMBDA, n[0], rhs);
- Debug("boolean-terms") << "rewrote " << n << " as " << out << std::endl;
- Debug("boolean-terms") << "need type " << asType << endl;
- // Assert(out.getType() == asType);
- return out;
- }
- if(!n.isConst()) {
- // we don't handle non-const right now
- return n;
- }
- if(asType.isBoolean()) {
- if(n.getType().isBitVector(1u)) {
- // type mismatch: should only happen for Boolean-term conversion under
- // datatype constructor applications; rewrite from BV(1) back to Boolean
- bool tf = (n.getConst<BitVector>().getValue() == 1);
- return NodeManager::currentNM()->mkConst(tf);
- }
- if(n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())) {
- // type mismatch: should only happen for Boolean-term conversion under
- // datatype constructor applications; rewrite from datatype back to Boolean
- Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
- Assert(n.getNumChildren() == 0);
- // we assume (by construction) false is first; see boolean_terms.cpp
- bool tf = (Datatype::indexOf(n.getOperator().toExpr()) == 1);
- Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << " ==> " << tf << endl;
- return NodeManager::currentNM()->mkConst(tf);
- }
- }
- if(n.getType().isBoolean()) {
- bool tf = n.getConst<bool>();
- if(asType.isBitVector(1u)) {
- return NodeManager::currentNM()->mkConst(BitVector(1u, tf ? 1u : 0u));
- }
- if(asType.isDatatype() && asType.hasAttribute(BooleanTermAttr())) {
- const Datatype& asDatatype = asType.getDatatype();
- return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor());
- }
- }
- Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl;
- if(n.getType().isArray()) {
- Assert(asType.isArray());
- if(n.getKind() == kind::STORE) {
- return NodeManager::currentNM()->mkNode(kind::STORE,
- rewriteAs(n[0], asType),
- rewriteAs(n[1], asType[0]),
- rewriteAs(n[2], asType[1]));
- }
- Assert(n.getKind() == kind::STORE_ALL);
- const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
- Node val = rewriteAs(asa.getExpr(), asType[1]);
- return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType.toType(), val.toExpr()));
- }
- if( n.getType().isSet() ){
- if( n.getKind()==kind::UNION ){
- std::vector< Node > children;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- children.push_back( rewriteAs( n[i], asType ) );
- }
- return NodeManager::currentNM()->mkNode(kind::UNION,children);
- }
- }
- if(n.getType().isParametricDatatype() &&
- n.getType().isInstantiatedDatatype() &&
- asType.isParametricDatatype() &&
- asType.isInstantiatedDatatype() &&
- n.getType()[0] == asType[0]) {
- // Here, we're doing something like rewriting a (Pair BV1 BV1) as a
- // (Pair Bool Bool).
- const Datatype* dt2 = &asType[0].getDatatype();
- std::vector<TypeNode> fromParams, toParams;
- for(unsigned i = 0; i < dt2->getNumParameters(); ++i) {
- fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
- toParams.push_back(asType[i + 1]);
- }
- Assert(dt2 == &Datatype::datatypeOf(n.getOperator().toExpr()));
- size_t ctor_ix = Datatype::indexOf(n.getOperator().toExpr());
- NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
- appctorb << (*dt2)[ctor_ix].getConstructor();
- for(size_t j = 0; j < n.getNumChildren(); ++j) {
- TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[ctor_ix][j].getSelector().getType()).getRangeType());
- asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
- appctorb << rewriteAs(n[j], asType);
- }
- Node out = appctorb;
- return out;
- }
- if(asType.getNumChildren() != n.getNumChildren() ||
- n.getMetaKind() == kind::metakind::CONSTANT) {
- return n;
- }
- NodeBuilder<> b(n.getKind());
- if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
- b << n.getOperator();
- }
- TypeNode::iterator t = asType.begin();
- for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) {
- Assert(t != asType.end());
- b << rewriteAs(*i, *t);
- }
- Assert(t == asType.end());
- Debug("boolean-terms") << "+++ constructing " << b << endl;
- Node out = b;
- return out;
-}
-
-void ModelPostprocessor::visit(TNode current, TNode parent) {
- Debug("tuprec") << "visiting " << current << endl;
- Assert(!alreadyVisited(current, TNode::null()));
- bool rewriteChildren = false;
- if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
- ( current.getOperator().hasAttribute(BooleanTermAttr()) ||
- ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION &&
- current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) {
- NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
- Node realOp;
- if(current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION) {
- TNode oldAsc = current.getOperator().getOperator();
- Debug("boolean-terms") << "old asc: " << oldAsc << endl;
- Node newCons = current.getOperator()[0].getAttribute(BooleanTermAttr());
- Node newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().toType()));
- Debug("boolean-terms") << "new asc: " << newAsc << endl;
- if(newCons.getType().getRangeType().isParametricDatatype()) {
- vector<TypeNode> oldParams = TypeNode::fromType(oldAsc.getConst<AscriptionType>().getType()).getRangeType().getParamTypes();
- vector<TypeNode> newParams = newCons.getType().getRangeType().getParamTypes();
- Assert(oldParams.size() == newParams.size() && oldParams.size() > 0);
- newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().substitute(newParams.begin(), newParams.end(), oldParams.begin(), oldParams.end()).toType()));
- }
- realOp = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, newAsc, newCons);
- } else {
- realOp = current.getOperator().getAttribute(BooleanTermAttr());
- }
- b << realOp;
- Debug("boolean-terms") << "+ op " << b.getOperator() << endl;
- TypeNode::iterator j = realOp.getType().begin();
- for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++j) {
- Assert(j != realOp.getType().end());
- Assert(alreadyVisited(*i, TNode::null()));
- TNode repl = d_nodes[*i];
- repl = repl.isNull() ? *i : repl;
- Debug("boolean-terms") << "+ adding " << repl << " expecting " << *j << endl;
- b << rewriteAs(repl, *j);
- }
- Node n = b;
- Debug("boolean-terms") << "model-post: " << current << endl
- << "- returning " << n << endl;
- d_nodes[current] = n;
- return;
- //all kinds with children that can occur in nodes in a model go here
- } else if(current.getKind() == kind::LAMBDA || current.getKind() == kind::SINGLETON || current.getKind() == kind::UNION ||
- current.getKind()==kind::STORE || current.getKind()==kind::STORE_ALL || current.getKind()==kind::APPLY_CONSTRUCTOR ) {
- rewriteChildren = true;
- }
- if( rewriteChildren ){
- // rewrite based on children
- bool self = true;
- for(size_t i = 0; i < current.getNumChildren(); ++i) {
- Assert(d_nodes.find(current[i]) != d_nodes.end());
- if(!d_nodes[current[i]].isNull()) {
- self = false;
- break;
- }
- }
- if(self) {
- Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
- // rewrite to self
- d_nodes[current] = Node::null();
- } else {
- // rewrite based on children
- NodeBuilder<> nb(current.getKind());
- if(current.getMetaKind() == kind::metakind::PARAMETERIZED) {
- TNode op = current.getOperator();
- Node realOp;
- if(op.getAttribute(BooleanTermAttr(), realOp)) {
- nb << realOp;
- } else {
- nb << op;
- }
- }
- for(size_t i = 0; i < current.getNumChildren(); ++i) {
- Assert(d_nodes.find(current[i]) != d_nodes.end());
- TNode rw = d_nodes[current[i]];
- if(rw.isNull()) {
- rw = current[i];
- }
- nb << rw;
- }
- d_nodes[current] = nb;
- Debug("tuprec") << "rewrote children for kind " << current.getKind() << " got " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
- }
- } else {
- Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
- // rewrite to self
- d_nodes[current] = Node::null();
- }
-}/* ModelPostprocessor::visit() */
} /* namespace smt */
} /* namespace CVC4 */
namespace CVC4 {
namespace smt {
-class ModelPostprocessor {
- std::hash_map<TNode, Node, TNodeHashFunction> d_nodes;
-
-public:
- typedef Node return_type;
-
- Node rewriteAs(TNode n, TypeNode asType);
-
- bool alreadyVisited(TNode current, TNode parent) {
- return d_nodes.find(current) != d_nodes.end();
- }
-
- void visit(TNode current, TNode parent);
-
- void start(TNode n) { }
-
- Node done(TNode n) {
- Assert(alreadyVisited(n, TNode::null()));
- TNode retval = d_nodes[n];
- return retval.isNull() ? n : retval;
- }
-};/* class ModelPostprocessor */
}/* CVC4::smt namespace */
}/* CVC4 namespace */
struct SmtEngineStatistics {
/** time spent in definition-expansion */
TimerStat d_definitionExpansionTime;
- /** time spent in Boolean term rewriting */
- TimerStat d_rewriteBooleanTermsTime;
/** time spent in non-clausal simplification */
TimerStat d_nonclausalSimplificationTime;
/** time spent in miplib pass */
SmtEngineStatistics() :
d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
- d_rewriteBooleanTermsTime("smt::SmtEngine::rewriteBooleanTermsTime"),
d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
d_miplibPassTime("smt::SmtEngine::miplibPassTime"),
d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0),
{
smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
- smtStatisticsRegistry()->registerStat(&d_rewriteBooleanTermsTime);
smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime);
smtStatisticsRegistry()->registerStat(&d_miplibPassTime);
smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved);
~SmtEngineStatistics() {
smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
- smtStatisticsRegistry()->unregisterStat(&d_rewriteBooleanTermsTime);
smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime);
smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime);
smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved);
/** Size of assertions array when preprocessing starts */
unsigned d_realAssertionsEnd;
- /** The converter for Boolean terms -> BITVECTOR(1). */
- BooleanTermConverter* d_booleanTermConverter;
-
/** A circuit propagator for non-clausal propositional deduction */
booleans::CircuitPropagator d_propagator;
bool d_propagatorNeedsFinish;
IteSkolemMap d_iteSkolemMap;
/** Instance of the ITE remover */
- RemoveITE d_iteRemover;
+ RemoveTermFormulas d_iteRemover;
private:
d_listenerRegistrations(new ListenerRegistrationList()),
d_nonClausalLearnedLiterals(),
d_realAssertionsEnd(0),
- d_booleanTermConverter(NULL),
d_propagator(d_nonClausalLearnedLiterals, true, true),
d_propagatorNeedsFinish(false),
d_assertions(),
d_propagator.finish();
d_propagatorNeedsFinish = false;
}
- if(d_booleanTermConverter != NULL) {
- delete d_booleanTermConverter;
- d_booleanTermConverter = NULL;
- }
d_smt.d_nodeManager->unsubscribeEvents(this);
}
bool expandOnly = false)
throw(TypeCheckingException, LogicException, UnsafeInterruptException);
- /**
- * Rewrite Boolean terms in a Node.
- */
- Node rewriteBooleanTerms(TNode n);
-
/**
* Simplify node "in" by expanding definitions and applying any
* substitutions learned from preprocessing.
d_logic = log;
d_logic.lock();
}
+ if(d_logic.isTheoryEnabled(THEORY_ARRAY) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_SETS)) {
+ if(!d_logic.isTheoryEnabled(THEORY_UF)) {
+ LogicInfo log(d_logic.getUnlockedCopy());
+ Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl;
+ log.enableTheory(THEORY_UF);
+ d_logic = log;
+ d_logic.lock();
+ }
+ }
// by default, symmetry breaker is on only for QF_UF
if(! options::ufSymmetryBreaker.wasSetByUser()) {
for (; pos != newSubstitutions.end(); ++pos) {
// Add back this substitution as an assertion
TNode lhs = (*pos).first, rhs = newSubstitutions.apply((*pos).second);
- Node n = NodeManager::currentNM()->mkNode(lhs.getType().isBoolean() ? kind::IFF : kind::EQUAL, lhs, rhs);
+ Node n = NodeManager::currentNM()->mkNode(kind::EQUAL, lhs, rhs);
substitutionsBuilder << n;
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl;
}
return false;
}
-Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) {
- TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
-
- spendResource(options::preprocessStep());
-
- if(d_booleanTermConverter == NULL) {
- // This needs to be initialized _after_ the whole SMT framework is in place, subscribed
- // to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype
- // definition, and not dump it properly.
- d_booleanTermConverter = new BooleanTermConverter(d_smt);
- }
- Node retval = d_booleanTermConverter->rewriteBooleanTerms(n);
- if(retval != n) {
- switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) {
- case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
- case booleans::BOOLEAN_TERM_CONVERT_NATIVE:
- if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) {
- d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
- d_smt.d_logic.enableTheory(THEORY_BV);
- d_smt.d_logic.lock();
- }
- break;
- case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
- if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) {
- d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
- d_smt.d_logic.enableTheory(THEORY_DATATYPES);
- d_smt.d_logic.lock();
- }
- break;
- default:
- Unhandled(mode);
- }
- }
- return retval;
-}
-
void SmtEnginePrivate::processAssertions() {
TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
spendResource(options::preprocessStep());
dumpAssertions("post-bv-abstraction", d_assertions);
}
- dumpAssertions("pre-boolean-terms", d_assertions);
- {
- Chat() << "rewriting Boolean terms..." << endl;
- for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) {
- d_assertions.replace(i, rewriteBooleanTerms(d_assertions[i]));
- }
- }
- dumpAssertions("post-boolean-terms", d_assertions);
-
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
dumpAssertions("pre-constrain-subtypes", d_assertions);
}/* SmtEngine::assertFormula() */
Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
+/*
ModelPostprocessor mpost;
NodeVisitor<ModelPostprocessor> visitor;
Node value = visitor.run(mpost, node);
Debug("boolean-terms") << "postproc: after rewrite " << realValue << endl;
}
return realValue;
+ */
+ return node;
}
Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
// used by the Model classes. It's not clear to me exactly how these
// two are different, but they need to be unified. This ugly hack here
// is to fix bug 554 until we can revamp boolean-terms and models [MGD]
+
+ //AJR : necessary?
if(!n.getType().isFunction()) {
- n = d_private->rewriteBooleanTerms(n);
n = Rewriter::rewrite(n);
}
// Expand, then normalize
hash_map<Node, Node, NodeHashFunction> cache;
Node n = d_private->expandDefinitions(*i, cache);
- n = d_private->rewriteBooleanTerms(n);
n = Rewriter::rewrite(n);
Trace("smt") << "--- getting value of " << n << endl;
}
void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
- if (t1.getKind() == kind::CONST_BOOLEAN) {
- d_acm.propagate(t1.iffNode(t2));
- } else {
- d_acm.propagate(t1.eqNode(t2));
- }
+ d_acm.propagate(t1.eqNode(t2));
}
void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyNewClass(TNode t) {
d_acm.eqNotifyNewClass(t);
for (j = leftWrites - 1; j > i; --j) {
index_j = write_j[1];
if (!ppCheck || !ppDisequal(index_i, index_j)) {
- Node hyp2(index_i.getType() == nm->booleanType()?
- index_i.iffNode(index_j) : index_i.eqNode(index_j));
+ Node hyp2(index_i.eqNode(index_j));
hyp << hyp2.notNode();
}
write_j = write_j[0];
}
Node r1 = nm->mkNode(kind::SELECT, e1, index_i);
- conc = (r1.getType() == nm->booleanType())?
- r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]);
+ conc = r1.eqNode(write_i[2]);
if (hyp.getNumChildren() != 0) {
if (hyp.getNumChildren() == 1) {
conc = hyp.getChild(0).impNode(conc);
case kind::NOT:
{
d_ppFacts.push_back(in);
- Assert(in[0].getKind() == kind::EQUAL ||
- in[0].getKind() == kind::IFF );
+ Assert(in[0].getKind() == kind::EQUAL );
Node a = in[0][0];
Node b = in[0][1];
d_ppEqualityEngine.assertEquality(in[0], false, in);
TNode atom = polarity ? literal : literal[0];
//eq::EqProof * eqp = new eq::EqProof;
// eq::EqProof * eqp = NULL;
- if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+ if (atom.getKind() == kind::EQUAL) {
d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, proof);
} else {
d_equalityEngine.explainPredicate(atom, polarity, assumptions, proof);
Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL;
- if (a.getKind() == kind::CONST_BOOLEAN) {
- d_conflictNode = explain(a.iffNode(b), proof);
- } else {
- d_conflictNode = explain(a.eqNode(b), proof);
- }
+ d_conflictNode = explain(a.eqNode(b), proof);
if (!d_inCheckModel) {
ProofArray* proof_array = NULL;
}
bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
- Unreachable();
+ Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
+ // Just forward to arrays
+ if (value) {
+ return d_arrays.propagate(predicate);
+ } else {
+ return d_arrays.propagate(predicate.notNode());
+ }
}
bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
void setMostFrequentValueCount(TNode store, uint64_t count);
static inline Node mkEqNode(Node a, Node b) {
- return a.getType().isBoolean() ? a.iffNode(b) : a.eqNode(b);
+ return a.eqNode(b);
}
class TheoryArraysRewriter {
}
break;
}
- case kind::EQUAL:
- case kind::IFF: {
+ case kind::EQUAL:{
if(node[0] == node[1]) {
Trace("arrays-postrewrite") << "Arrays::postRewrite returning true" << std::endl;
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
}
break;
}
- case kind::EQUAL:
- case kind::IFF: {
+ case kind::EQUAL:{
if(node[0] == node[1]) {
Trace("arrays-prerewrite") << "Arrays::preRewrite returning true" << std::endl;
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
}
}
break;
- case kind::IFF:
+ case kind::EQUAL:
+ Assert( parent[0].getType().isBoolean() );
if (parentAssignment) {
// IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment])
if (isAssigned(parent[0])) {
}
}
break;
- case kind::IFF:
+ case kind::EQUAL:
+ Assert( parent[0].getType().isBoolean() );
if (isAssigned(parent[0]) && isAssigned(parent[1])) {
// IFF x y: if x or y is assigned, assign(IFF = (x.assignment <=> y.assignment))
assignAndEnqueue(parent, getAssignment(parent[0]) == getAssignment(parent[1]));
operator NOT 1 "logical not"
operator AND 2: "logical and (N-ary)"
-operator IFF 2 "logical equivalence (exactly two parameters)"
operator IMPLIES 2 "logical implication (exactly two parameters)"
operator OR 2: "logical or (N-ary)"
operator XOR 2 "exclusive or (exactly two parameters)"
typerule NOT ::CVC4::theory::boolean::BooleanTypeRule
typerule AND ::CVC4::theory::boolean::BooleanTypeRule
-typerule IFF ::CVC4::theory::boolean::BooleanTypeRule
typerule IMPLIES ::CVC4::theory::boolean::BooleanTypeRule
typerule OR ::CVC4::theory::boolean::BooleanTypeRule
typerule XOR ::CVC4::theory::boolean::BooleanTypeRule
return PP_ASSERT_STATUS_SOLVED;
}
+/*
+void TheoryBool::check(Effort level) {
+ if (done() && !fullEffort(level)) {
+ return;
+ }
+ while (!done())
+ {
+ // Get all the assertions
+ Assertion assertion = get();
+ TNode fact = assertion.assertion;
+ Trace("ajr-bool") << "Assert : " << fact << std::endl;
+ }
+ if( Theory::fullEffort(level) ){
+ }
+}
+*/
}/* CVC4::theory::booleans namespace */
}/* CVC4::theory namespace */
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+ //void check(Effort);
+
std::string identify() const { return std::string("TheoryBool"); }
};/* class TheoryBool */
if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
break;
}
- case kind::IFF:
case kind::EQUAL: {
// rewrite simple cases of IFF
if(n[0] == tt) {
int parityTmp;
if ((parityTmp = equalityParity(n[1], n[2])) != 0) {
- Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].iffNode(n[1]);
+ Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].eqNode(n[1]);
Debug("bool-ite") << "equalityParity n[1], n[2] " << parityTmp
<< " " << n << ": " << resp << std::endl;
return RewriteResponse(REWRITE_AGAIN, resp);
if(in.getNumChildren() == 2) {
// if this is the case exactly 1 != pair will be generated so the
// AND is not required
- Node eq = NodeManager::currentNM()->mkNode(in[0].getType().isBoolean() ? kind::IFF : kind::EQUAL, in[0], in[1]);
+ Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, in[0], in[1]);
Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
return neq;
}
for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
TNode::iterator j = i;
while(++j != in.end()) {
- Node eq = NodeManager::currentNM()->mkNode((*i).getType().isBoolean() ? kind::IFF : kind::EQUAL, *i, *j);
+ Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, *i, *j);
Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
diseqs.push_back(neq);
}
throw TypeCheckingExceptionPrivate(n, ss.str());
}
-
- if ( lhsType == booleanType && rhsType == booleanType ) {
- throw TypeCheckingExceptionPrivate(n, "equality between two boolean terms (use IFF instead)");
- }
}
return booleanType;
}
}
break;
}
- case kind::IFF:
- {
- Assert (node.getNumChildren() == 2);
- Abc_Obj_t* child1 = bbFormula(node[0]);
- Abc_Obj_t* child2 = bbFormula(node[1]);
-
- result = mkIff(child1, child2);
- break;
- }
case kind::XOR:
{
result = bbFormula(node[0]);
result = mkInput(node);
break;
}
+ case kind::EQUAL:
+ {
+ if( node[0].getType().isBoolean() ){
+ Assert (node.getNumChildren() == 2);
+ Abc_Obj_t* child1 = bbFormula(node[0]);
+ Abc_Obj_t* child2 = bbFormula(node[1]);
+
+ result = mkIff(child1, child2);
+ break;
+ }
+ //else, continue...
+ }
default:
bbAtom(node);
result = getBBAtom(node);
template <> inline
Node mkIff<Node>(Node a, Node b) {
- return NodeManager::currentNM()->mkNode(kind::IFF, a, b);
+ return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
}
template <> inline
bool changed = subst.addSubstitution(var, new_right, reason);
if (Dump.isOn("bv-algebraic")) {
- Node query = utils::mkNot(utils::mkNode(kind::IFF, fact, utils::mkNode(kind::EQUAL, var, new_right)));
+ Node query = utils::mkNot(utils::mkNode(kind::EQUAL, fact, utils::mkNode(kind::EQUAL, var, new_right)));
Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
Dump("bv-algebraic") << PushCommand();
Dump("bv-algebraic") << AssertCommand(query.toExpr());
Assert (utils::getSize(node[1]) == 1);
Node a = convertBvTerm(node[0]);
Node b = convertBvTerm(node[1]);
- Node result = utils::mkNode(kind::IFF, a, b);
+ Node result = utils::mkNode(kind::EQUAL, a, b);
Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvAtom " << node <<" => " << result << "\n";
++(d_statistics.d_numAtomsLifted);
}
// asserting that the atom is true iff the definition holds
- Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
+ Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb);
AlwaysAssert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
storeBBAtom(node, atom_bb);
atom_bb = utils::mkAnd(atoms);
}
Assert (!atom_bb.isNull());
- Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
+ Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb);
storeBBAtom(node, atom_bb);
d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
return;
}
// asserting that the atom is true iff the definition holds
- Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
+ Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb);
storeBBAtom(node, atom_bb);
d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
}
std::ostringstream os;
os << "RewriteRule <"<<rule<<">; expect unsat";
- Node condition;
- if (result.getType().isBoolean()) {
- condition = node.iffNode(result).notNode();
- } else {
- condition = node.eqNode(result).notNode();
- }
+ Node condition = node.eqNode(result).notNode();
Dump("bv-rewrites")
<< CommentCommand(os.str())
Trace("datatypes-rewrite-debug") << "Clash constants : " << n1 << " " << n2 << std::endl;
return true;
}else{
- Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 );
+ Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n1, n2 );
rew.push_back( eq );
}
}
rt.d_req_kind = OR;reqk = NOT;
}else if( k==OR ){
rt.d_req_kind = AND;reqk = NOT;
- }else if( k==IFF ) {
+ //AJR : eliminate this if we eliminate xor
+ }else if( k==EQUAL ) {
rt.d_req_kind = XOR;
}else if( k==XOR ) {
- rt.d_req_kind = IFF;
+ rt.d_req_kind = EQUAL;
}else if( k==ITE ){
rt.d_req_kind = ITE;reqkc[1] = NOT;reqkc[2] = NOT;
rt.d_children[0].d_req_type = d_tds->getArgType( dt[c], 0 );
bool SygusSymBreak::processConstantArg( TypeNode tnp, const Datatype & pdt, int pc,
Kind k, int i, Node arg, std::map< unsigned, bool >& rlv ) {
Assert( d_tds->hasKind( tnp, k ) );
- if( k==AND || k==OR || k==IFF || k==XOR || k==IMPLIES || ( k==ITE && i==0 ) ){
+ if( k==AND || k==OR || ( k==EQUAL && arg.getType().isBoolean() ) || k==XOR || k==IMPLIES || ( k==ITE && i==0 ) ){
return false;
}else if( d_tds->isIdempotentArg( arg, k, i ) ){
if( pdt[pc].getNumArgs()==2 ){
//do all pending merges
int i=0;
while( i<(int)d_pending_merge.size() ){
- Assert( d_pending_merge[i].getKind()==EQUAL || d_pending_merge[i].getKind()==IFF );
+ Assert( d_pending_merge[i].getKind()==EQUAL );
merge( d_pending_merge[i][0], d_pending_merge[i][1] );
i++;
}
d_equalityEngine.addTriggerPredicate(n);
break;
default:
- // Maybe it's a predicate
- if (n.getType().isBoolean()) {
- // Get triggered for both equal and dis-equal
- d_equalityEngine.addTriggerPredicate(n);
- } else {
- // Function applications/predicates
- d_equalityEngine.addTerm(n);
- //d_equalityEngine.addTriggerTerm(n, THEORY_DATATYPES);
- }
+ // Function applications/predicates
+ d_equalityEngine.addTerm(n);
+ //d_equalityEngine.addTriggerTerm(n, THEORY_DATATYPES);
break;
}
flushPendingFacts();
void TheoryDatatypes::addSharedTerm(TNode t) {
Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
<< t << " " << t.getType().isBoolean() << endl;
- //if( t.getType().isBoolean() ){
- //d_equalityEngine.addTriggerPredicate(t, THEORY_DATATYPES);
- //}else{
d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES);
- //}
Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl;
}
Debug("datatypes-explain") << "Explain " << literal << std::endl;
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
- if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+ if (atom.getKind() == kind::EQUAL) {
explainEquality( atom[0], atom[1], polarity, assumptions );
} else if( atom.getKind() == kind::AND && polarity ){
for( unsigned i=0; i<atom.getNumChildren(); i++ ){
/** Conflict when merging two constants */
void TheoryDatatypes::conflict(TNode a, TNode b){
- if (a.getKind() == kind::CONST_BOOLEAN) {
- d_conflictNode = explain( a.iffNode(b) );
- } else {
- d_conflictNode = explain( a.eqNode(b) );
- }
+ d_conflictNode = explain( a.eqNode(b) );
Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl;
d_out->conflict( d_conflictNode );
d_conflict = true;
for( unsigned i=0; i<deq_cand.size(); i++ ){
if( d_equalityEngine.areDisequal( deq_cand[i].first, deq_cand[i].second, true ) ){
conf = true;
- Node eq = NodeManager::currentNM()->mkNode( deq_cand[i].first.getType().isBoolean() ? kind::IFF : kind::EQUAL,
- deq_cand[i].first, deq_cand[i].second );
+ Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, deq_cand[i].first, deq_cand[i].second );
exp.push_back( eq.negate() );
}
}
//do unification
for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
if( !areEqual( cons1[i], cons2[i] ) ){
- Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] );
+ Node eq = cons1[i].eqNode( cons2[i] );
d_pending.push_back( eq );
d_pending_exp[ eq ] = unifEq;
Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " << unifEq << std::endl;
if( !r.isNull() ){
Node rr = Rewriter::rewrite( r );
if( use_s!=rr ){
- Node eq = rr.getType().isBoolean() ? use_s.iffNode( rr ) : use_s.eqNode( rr );
+ Node eq = use_s.eqNode( rr );
Node eq_exp;
if( options::dtRefIntro() ){
eq_exp = d_true;
if( children.empty() ){
lem = n.negate();
}else{
- lem = NodeManager::currentNM()->mkNode( IFF, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) );
+ lem = NodeManager::currentNM()->mkNode( EQUAL, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) );
}
Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl;
//d_pending.push_back( lem );
//see if it is rewritten to be something different
Node rn = Rewriter::rewrite( n );
if( rn!=n && !areEqual( rn, n ) ){
- Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n );
+ Node eq = rn.eqNode( n );
d_pending.push_back( eq );
d_pending_exp[ eq ] = d_true;
Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl;
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
addLemma = dt.involvesExternalType();
}
- }else if( n.getKind()==LEQ || n.getKind()==IFF || n.getKind()==OR ){
+ }else if( n.getKind()==LEQ || n.getKind()==OR ){
addLemma = true;
}
if( addLemma ){
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
while( !eqcs_i.isFinished() ){
Node eqc = (*eqcs_i);
- if( !eqc.getType().isBoolean() ){
+ //if( !eqc.getType().isBoolean() ){
if( eqc.getType().isDatatype() ){
Trace( c ) << "DATATYPE : ";
}
Trace( c ) << std::endl;
}
}
- }
+ //}
++eqcs_i;
}
}
d_compressed[original] = skolem;
d_compressed[compressed] = skolem;
- Node iff = skolem.iffNode(rewritten);
+ Node iff = skolem.eqNode(rewritten);
d_assertions->push_back(iff);
++(d_statistics.d_skolemsAdded);
return skolem;
Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
Trace("alpha-eq") << " " << q << std::endl;
Trace("alpha-eq") << " " << aen->d_quant << std::endl;
- lem = q.iffNode( aen->d_quant );
+ lem = q.eqNode( aen->d_quant );
}else{
//do not reduce annotated quantified formulas based on alpha equivalence
}
if( d_ranges_proxied.find( curr )==d_ranges_proxied.end() ){
d_ranges_proxied[curr] = true;
Assert( d_range_literal.find( curr )!=d_range_literal.end() );
- Node lem = NodeManager::currentNM()->mkNode( IFF, d_range_literal[curr].negate(),
+ Node lem = NodeManager::currentNM()->mkNode( EQUAL, d_range_literal[curr].negate(),
NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(curr) ) ) );
Trace("bound-int-lemma") << "*** bound int : proxy lemma : " << lem << std::endl;
d_bi->getQuantifiersEngine()->addLemma( lem );
CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
CandidateGenerator( qe ), d_match_pattern( mpat ){
- Assert( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF );
+ Assert( d_match_pattern.getKind()==EQUAL );
d_match_pattern_type = d_match_pattern[0].getType();
}
}
for( unsigned j=1; j<n.getNumChildren(); j++ ){
Node nc = getEagerUnfold( n[j], visited );
- if( var_list[j-1].getType().isBoolean() ){
- //TODO: remove this case when boolean term conversion is eliminated
- Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
- subs.push_back( nc.eqNode( c ) );
- }else{
- subs.push_back( nc );
- }
+ //if( var_list[j-1].getType().isBoolean() ){
+ // //TODO: remove this case when boolean term conversion is eliminated
+ // Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+ // subs.push_back( nc.eqNode( c ) );
+ //}else{
+ subs.push_back( nc );
+ //}
Assert( subs[j-1].getType()==var_list[j-1].getType() );
}
Assert( vars.size()==subs.size() );
Assert( d_single_inv_arg_sk.size()==varList.getNumChildren() );
for( unsigned i=0; i<d_single_inv_arg_sk.size(); i++ ){
Trace("csi-sol") << d_single_inv_arg_sk[i] << " ";
- if( varList[i].getType().isBoolean() ){
- //TODO force boolean term conversion mode
- Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
- vars.push_back( d_single_inv_arg_sk[i].eqNode( c ) );
- }else{
- vars.push_back( d_single_inv_arg_sk[i] );
- }
+ //if( varList[i].getType().isBoolean() ){
+ // //TODO force boolean term conversion mode
+ // Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+ // vars.push_back( d_single_inv_arg_sk[i].eqNode( c ) );
+ //}else{
+ vars.push_back( d_single_inv_arg_sk[i] );
+ //}
d_sol->d_varList.push_back( varList[i] );
}
Trace("csi-sol") << std::endl;
if( n0.getKind()==ITE ){
n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
NodeManager::currentNM()->mkNode( AND, n0.negate(), n2 ) );
- }else if( n0.getKind()==IFF ){
+ }else if( n0.getKind()==EQUAL ){
n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
NodeManager::currentNM()->mkNode( AND, n0.negate(), n1.negate() ) );
}else{
}
}else if( n.getKind()==NOT ){
return getAssign( !pol, n[0], assign, new_assign, vars, new_vars, new_subs );
- }else if( pol && ( n.getKind()==IFF || n.getKind()==EQUAL ) ){
+ }else if( pol && n.getKind()==EQUAL ){
getAssignEquality( n, vars, new_vars, new_subs );
}
}
}
bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs ) {
- Assert( eq.getKind()==IFF || eq.getKind()==EQUAL );
+ Assert( eq.getKind()==EQUAL );
//try to find valid argument
for( unsigned r=0; r<2; r++ ){
if( std::find( d_varList.begin(), d_varList.end(), eq[r] )!=d_varList.end() ){
std::map< Node, bool >::iterator it = atoms.find( atom );
if( it==atoms.end() ){
atoms[atom] = pol;
- if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){
+ if( status==0 && atom.getKind()==EQUAL ){
if( pol==( sol.getKind()==AND ) ){
Trace("csi-simp") << " ...equality." << std::endl;
if( getAssignEquality( atom, vars, new_vars, new_subs ) ){
bool red = false;
Node atom = children[i].getKind()==NOT ? children[i][0] : children[i];
bool pol = children[i].getKind()!=NOT;
- if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){
+ if( status==0 && atom.getKind()==EQUAL ){
if( pol!=( sol.getKind()==AND ) ){
std::vector< Node > tmp_vars;
std::vector< Node > tmp_subs;
Node new_t;
do{
new_t = Node::null();
- if( curr.getKind()==EQUAL && ( curr[0].getType().isInteger() || curr[0].getType().isReal() ) ){
- new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ),
- NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) );
+ if( curr.getKind()==EQUAL ){
+ if( curr[0].getType().isInteger() || curr[0].getType().isReal() ){
+ new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ),
+ NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) );
+ }else if( curr[0].getType().isBoolean() ){
+ new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
+ NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) );
+ }else{
+ new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) );
+ }
}else if( curr.getKind()==ITE ){
new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) );
- }else if( curr.getKind()==IFF ){
- new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
- NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) );
}else if( curr.getKind()==OR || curr.getKind()==AND ){
new_t = TermDb::simpleNegate( curr ).negate();
}else if( curr.getKind()==NOT ){
Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl;
}
}
+ }else if( atom.getKind()==BOOLEAN_TERM_VARIABLE ){
+ if( std::find( d_aux_vars.begin(), d_aux_vars.end(), atom )!=d_aux_vars.end() ){
+ Node val = NodeManager::currentNM()->mkConst( lit.getKind()!=NOT );
+ aux_subs[ atom ] = val;
+ Trace("cbqi-proc") << "......add substitution : " << atom << " -> " << val << std::endl;
+ }
}
}
}
d_is_nested_quant = true;
}else if( visited.find( n )==visited.end() ){
visited[n] = true;
- if( TermDb::isBoolConnective( n.getKind() ) ){
+ if( TermDb::isBoolConnectiveTerm( n ) ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
collectCeAtoms( n[i], visited );
}
//remove ITEs
IteSkolemMap iteSkolemMap;
- d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
+ d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap);
//Assert( d_aux_vars.empty() );
d_aux_vars.clear();
d_aux_eq.clear();
}
}
}
+ /*else if( lems[i].getKind()==EQUAL && lems[i][0].getType().isBoolean() ){
+ //Boolean terms
+ if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][0] )!=d_aux_vars.end() ){
+ Node v = lems[i][0];
+ d_aux_eq[rlem][v] = lems[i][1];
+ Trace("cbqi-debug") << " " << rlem << " implies " << v << " = " << lems[i][1] << std::endl;
+ }
+ }*/
lems[i] = rlem;
}
//collect atoms from all lemmas: we will only do bounds coming from original body
}else{
return 0;
}
- }else if( n.getKind()==IFF ){
+ }else if( n.getKind()==EQUAL && n[0].getType().isBoolean() ){
int depIndex1;
int eVal = evaluate( n[0], depIndex1, ri );
if( eVal!=0 ){
Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl;
if( !bd.isNull() ){
d_funcs.push_back( f );
- bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd );
+ bd = NodeManager::currentNM()->mkNode( EQUAL, n, bd );
//create a sort S that represents the inputs of the function
std::stringstream ss;
for( unsigned i=0; i<assertions.size(); i++ ){
int is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end() ? 1 : 0;
//constant boolean function definitions do not add domain constraints
- if( is_fd==0 || ( is_fd==1 && ( assertions[i][1].getKind()==EQUAL || assertions[i][1].getKind()==IFF ) ) ){
+ if( is_fd==0 || ( is_fd==1 && assertions[i][1].getKind()==EQUAL ) ){
std::vector< Node > constraints;
Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl;
Node n = simplifyFormula( assertions[i], true, true, constraints, is_fd==1 ? subs_head[i] : Node::null(), is_fd );
std::vector< Node > children;
for( unsigned j=0; j<n.getNumChildren(); j++ ){
Node uz = NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], z );
- if( !n[j].getType().isBoolean() ){
- children.push_back( uz.eqNode( n[j] ) );
- }else{
- children.push_back( uz.iffNode( n[j] ) );
- }
+ children.push_back( uz.eqNode( n[j] ) );
}
Node bd = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );
bd = bd.negate();
unsigned ngtt = qe->getTermDatabase()->getNumTypeGroundTerms( tn );
Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl;
return ngtt;
-// }else if( d_match_pattern_getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
+// }else if( d_match_pattern_getKind()==EQUAL ){
}else{
return -1;
//we want to add the children of the NOT
d_match_pattern = d_pattern[0];
}
- if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
+ if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
//make sure the matching portion of the equality is on the LHS of d_pattern
// and record what d_match_pattern is
for( unsigned i=0; i<2; i++ ){
//we will be scanning lists trying to find d_match_pattern.getOperator()
d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern );
//if matching on disequality, inform the candidate generator not to match on eqc
- if( d_pattern.getKind()==NOT && ( d_pattern[0].getKind()==IFF || d_pattern[0].getKind()==EQUAL ) ){
+ if( d_pattern.getKind()==NOT && d_pattern[0].getKind()==EQUAL ){
((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel );
d_eq_class_rel = Node::null();
}
}else{
d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
}
- }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) &&
+ }else if( d_match_pattern.getKind()==EQUAL &&
d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){
//we will be producing candidates via literal matching heuristics
if( d_pattern.getKind()!=NOT ){
}
}else{
if( pat.getKind()==EQUAL ){
- Assert( t.getType().isReal() );
- t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one);
- }else if( pat.getKind()==IFF ){
- t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermDatabase()->d_true, t ) );
+ if( t.getType().isBoolean() ){
+ t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermDatabase()->d_true, t ) );
+ }else{
+ Assert( t.getType().isReal() );
+ t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one);
+ }
}else if( pat.getKind()==GEQ ){
t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one);
}else if( pat.getKind()==GT ){
}else{
d_pol = true;
}
- if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
+ if( d_match_pattern.getKind()==EQUAL ){
d_eqc = d_match_pattern[1];
d_match_pattern = d_match_pattern[0];
Assert( !quantifiers::TermDb::hasInstConstAttr( d_eqc ) );
return false;
}else{
Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();
- Assert( ak!=NOT );
- return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE;
+ if( ak==EQUAL ){
+ Node atom = n.getKind() ? n[0] : n;
+ return !atom[0].getType().isBoolean();
+ }else{
+ Assert( ak!=NOT );
+ return ak!=AND && ak!=OR && ak!=ITE;
+ }
}
}
addArgument( c, args, watch, is_watch );
abort_i = i;
break;
- }else if( k==kind::AND || k==kind::OR || k==kind::ITE || k==IFF ){
+ }else if( k==kind::AND || k==kind::OR || k==kind::ITE || ( k==EQUAL && n[0].getType().isBoolean() ) ){
Trace("qip-eval-debug") << "Adding argument " << c << " to " << k << ", isProp = " << newHasPol << std::endl;
if( ( k==kind::AND || k==kind::OR ) && c.getKind()==k ){
//flatten
Assert( index<(int)d_nested_qe_waitlist[q].size() );
Node nq = d_nested_qe_waitlist[q][index];
Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts );
- Node dqelem = nq.iffNode( nqeqn );
+ Node dqelem = nq.eqNode( nqeqn );
Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl;
d_quantEngine->getOutputChannel().lemma( dqelem );
d_nested_qe_waitlist_proc[q] = index + 1;
Assert( Trigger::isAtomicTrigger( pat ) );
if( pat.getType().isBoolean() && rpoleq.isNull() ){
if( options::literalMatchMode()==LITERAL_MATCH_USE ){
- pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
+ pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
}else if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){
- pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==1 ) );
+ pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==1 ) );
}
}else{
Assert( !rpoleq.isNull() );
}
bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
- return pol && ( n.getKind()==EQUAL || n.getKind()==IFF );
+ return pol && n.getKind()==EQUAL;
}
bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
}
Node QuantifierMacros::solveInEquality( Node n, Node lit ){
- if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
+ if( lit.getKind()==EQUAL ){
//return the opposite side of the equality if defined that way
for( int i=0; i<2; i++ ){
if( lit[i]==n ){
std::vector< Node > tr_terms;
if( lit.getKind()==APPLY_UF ){
//only match predicates that are contrary to this one, use literal matching
- Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false );
+ Node eq = NodeManager::currentNM()->mkNode( EQUAL, lit, !phase ? fm->d_true : fm->d_false );
tr_terms.push_back( eq );
}else if( lit.getKind()==EQUAL ){
//collect trigger terms
if( n.getKind()==FORALL ){
//TODO?
return true;
- }else if( n.getKind()==NOT || n.getKind()==AND || n.getKind()==OR || n.getKind()==EQUAL || n.getKind()==ITE || n.getKind()==IFF ){
+ }else if( n.getKind()==NOT || n.getKind()==AND || n.getKind()==OR || n.getKind()==EQUAL || n.getKind()==ITE ||
+ ( n.getKind()==EQUAL && n[0].getType().isBoolean() ) ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( !isPropagatingInstance( p, n[i] ) ){
return false;
void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) {
Trace("qcf-qregister-debug") << "Determine variable order " << d_n << ", #bvars = " << bvars.size() << std::endl;
- bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF );
+ bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==EQUAL );
if( isComm ){
std::map< int, std::vector< int > > c_to_vars;
std::map< int, std::vector< int > > vars_to_c;
success = true;
}
}
- }else if( d_n.getKind()==IFF ){
+ }else if( d_n.getKind()==EQUAL ){
//construct match based on both children
if( d_child_counter%2==0 ){
if( getChild( 0 )->getNextMatch( p, qi ) ){
}else{
return getChild( d_child_counter )->getExplanation( p, qi, exp );
}
- }else if( d_n.getKind()==IFF ){
+ }else if( d_n.getKind()==EQUAL ){
for( unsigned i=0; i<2; i++ ){
if( !getChild( i )->getExplanation( p, qi, exp ) ){
return false;
}
bool MatchGen::isHandledBoolConnective( TNode n ) {
- return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() ) && n.getKind()!=SEP_STAR;
+ return TermDb::isBoolConnectiveTerm( n ) && n.getKind()!=SEP_STAR;
}
bool MatchGen::isHandledUfTerm( TNode n ) {
}
Node QuantConflictFind::mkEqNode( Node a, Node b ) {
- if( a.getType().isBoolean() ){
- return a.iffNode( b );
- }else{
- return a.eqNode( b );
- }
+ return a.eqNode( b );
}
//-------------------------------------------------- registration
bool success = true;
Node t1;
Node t2;
- if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL || lit.getKind()==IFF ){
+ if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){
lit = getTermDatabase()->getCanonicalTerm( lit );
Trace("qee-debug") << "Canonical : " << lit << ", pol = " << pol << std::endl;
if( lit.getKind()==APPLY_UF ){
pol = true;
lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
}else if( lit.getKind()==EQUAL ){
- t1 = lit[0];
- t2 = lit[1];
- }else if( lit.getKind()==IFF ){
- if( lit[0].getKind()==NOT ){
- t1 = lit[0][0];
- pol = !pol;
+ if( lit[0].getType().isBoolean() ){
+ if( lit[0].getKind()==NOT ){
+ t1 = lit[0][0];
+ pol = !pol;
+ }else{
+ t1 = lit[0];
+ }
+ if( lit[1].getKind()==NOT ){
+ t2 = lit[1][0];
+ pol = !pol;
+ }else{
+ t2 = lit[1];
+ }
+ if( t1.getKind()==APPLY_UF && t2.getKind()==APPLY_UF ){
+ t1 = getFunctionAppForPredicateApp( t1 );
+ t2 = getFunctionAppForPredicateApp( t2 );
+ lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
+ }else{
+ success = false;
+ }
}else{
t1 = lit[0];
- }
- if( lit[1].getKind()==NOT ){
- t2 = lit[1][0];
- pol = !pol;
- }else{
t2 = lit[1];
}
- if( t1.getKind()==APPLY_UF && t2.getKind()==APPLY_UF ){
- t1 = getFunctionAppForPredicateApp( t1 );
- t2 = getFunctionAppForPredicateApp( t2 );
- lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
- }else{
- success = false;
- }
}
}else{
success = false;
}
Node QuantArith::solveEqualityFor( Node lit, Node v ) {
- Assert( lit.getKind()==EQUAL || lit.getKind()==IFF );
+ Assert( lit.getKind()==EQUAL );
//first look directly at sides
TypeNode tn = lit[0].getType();
for( unsigned r=0; r<2; r++ ){
std::vector< Node > disj;
Node x = NodeManager::currentNM()->mkBoundVar( tn );
for( unsigned i=0; i<d_consts[tn].size(); i++ ){
- disj.push_back( NodeManager::currentNM()->mkNode( tn.isBoolean() ? IFF : EQUAL, x, d_consts[tn][i] ) );
+ disj.push_back( NodeManager::currentNM()->mkNode( EQUAL, x, d_consts[tn][i] ) );
}
Assert( !disj.empty() );
d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ), disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ) );
case IMPLIES:
case XOR:
case ITE:
- case IFF:
return false;
break;
case EQUAL:
k = OR;
negCh1 = true;
}else if( ok==XOR ){
- k = IFF;
+ k = EQUAL;
negCh1 = true;
}else if( ok==NOT ){
if( body[0].getKind()==NOT ){
k = OR;
negAllCh = true;
body = body[0];
- }else if( body[0].getKind()==XOR || body[0].getKind()==IFF ){
- k = IFF;
- negCh1 = ( body[0].getKind()==IFF );
+ }else if( body[0].getKind()==XOR || ( body[0].getKind()==EQUAL && body[0][0].getType().isBoolean() ) ){
+ k = EQUAL;
+ negCh1 = ( body[0].getKind()==EQUAL );
body = body[0];
}else if( body[0].getKind()==ITE ){
k = body[0].getKind();
}else{
return body;
}
- }else if( ok!=IFF && ok!=ITE && ok!=AND && ok!=OR ){
+ }else if( ( ok!=EQUAL || !body[0].getType().isBoolean() ) && ok!=ITE && ok!=AND && ok!=OR ){
//a literal
return body;
}
}else if( res==-1 ){
return getEntailedCond( n[2], currCond );
}
- }else if( n.getKind()==IFF || n.getKind()==ITE ){
- unsigned start = n.getKind()==IFF ? 0 : 1;
+ }else if( ( n.getKind()==EQUAL && n[0].getType().isBoolean() ) || n.getKind()==ITE ){
+ unsigned start = n.getKind()==EQUAL ? 0 : 1;
int res1 = 0;
for( unsigned j=start; j<=(start+1); j++ ){
int res = getEntailedCond( n[j], currCond );
Assert( res!=0 );
if( n.getKind()==ITE ){
return res1==res ? res : 0;
- }else if( n.getKind()==IFF ){
+ }else if( n.getKind()==EQUAL ){
return res1==res ? 1 : -1;
}
}
Assert( !body.isNull() );
Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl;
Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds );
- return Rewriter::rewrite( NodeManager::currentNM()->mkNode( h.getType().isBoolean() ? IFF : EQUAL, h, r ) );
+ return Rewriter::rewrite( NodeManager::currentNM()->mkNode( EQUAL, h, r ) );
}else{
return computeProcessTerms2( body, true, true, curr_cond, 0, cache, icache, new_vars, new_conds );
}
}
}
if( options::condVarSplitQuant() ){
- if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() ) ){
+ if( body.getKind()==ITE || ( body.getKind()==EQUAL && body[0].getType().isBoolean() && options::condVarSplitQuantAgg() ) ){
Assert( !qa.isFunDef() );
Trace("quantifiers-rewrite-debug") << "Conditional var elim split " << body << "?" << std::endl;
bool do_split = false;
NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ),
NodeManager::currentNM()->mkNode( kind::OR, body[0], body[2] ) );
return computePrenex( nn, args, nargs, pol, prenexAgg );
- }else if( prenexAgg && body.getKind()==kind::IFF ){
+ }else if( prenexAgg && body.getKind()==kind::EQUAL && body[0].getType().isBoolean() ){
Node nn = NodeManager::currentNM()->mkNode( kind::AND,
NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ),
NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) );
case kind::RR_REWRITE:
// Equality
pattern.push_back( head );
- if( head.getType().isBoolean() ){
- body = head.iffNode(body);
- }else{
- body = head.eqNode(body);
- }
+ body = head.eqNode(body);
break;
case kind::RR_REDUCTION:
case kind::RR_DEDUCTION:
//check if it contains a quantifier as a subterm
//if so, we will write this node
if( containsQuantifiers( n ) ){
- if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || n.getKind()==kind::IFF ){
+ if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || ( n.getKind()==kind::EQUAL && n[0].getType().isBoolean() ) ){
if( options::preSkolemQuantAgg() ){
Node nn;
//must remove structure
nn = NodeManager::currentNM()->mkNode( kind::AND,
NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
- }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
+ }else if( n.getKind()==kind::EQUAL ){
nn = NodeManager::currentNM()->mkNode( kind::AND,
NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
- }else if( n.getKind()==kind::IMPLIES ){
- nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
}
return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
}
}
std::vector< Node > cc;
- //Node head = rr[2][0];
- //if( head!=d_true ){
- //Node head_eq = head.getType().isBoolean() ? head.iffNode( head ) : head.eqNode( head );
- //head_eq = head_eq.negate();
- //cc.push_back( head_eq );
- //Trace("rr-register-debug") << " head eq is " << head_eq << std::endl;
- //}
//add patterns
for( unsigned i=1; i<f[2].getNumChildren(); i++ ){
std::vector< Node > nc;
for( unsigned j=0; j<f[2][i].getNumChildren(); j++ ){
Node nn;
Node nbv = NodeManager::currentNM()->mkBoundVar( f[2][i][j].getType() );
- if( f[2][i][j].getType().isBoolean() ){
- if( f[2][i][j].getKind()!=APPLY_UF ){
- nn = f[2][i][j].negate();
- }else{
- nn = f[2][i][j].iffNode( nbv ).negate();
- bvl.push_back( nbv );
- }
- //nn = f[2][i][j].negate();
+ if( f[2][i][j].getType().isBoolean() && f[2][i][j].getKind()!=APPLY_UF ){
+ nn = f[2][i][j].negate();
}else{
nn = f[2][i][j].eqNode( nbv ).negate();
bvl.push_back( nbv );
}else{
if( at!=n && ee->areDisequal( at, n, false ) ){
std::vector< Node > lits;
- lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) );
+ lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at, n ) );
for( unsigned i=0; i<at.getNumChildren(); i++ ){
if( at[i]!=n[i] ){
- lits.push_back( NodeManager::currentNM()->mkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() );
+ lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at[i], n[i] ).negate() );
}
}
Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits );
Assert( !qy->extendsEngine() );
Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
Assert( n.getType().isBoolean() );
- if( n.getKind()==EQUAL ){
+ if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy );
if( !n1.isNull() ){
TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy );
}
}
return !simPol;
- }else if( n.getKind()==IFF || n.getKind()==ITE ){
+ //Boolean equality here
+ }else if( n.getKind()==EQUAL || n.getKind()==ITE ){
for( unsigned i=0; i<2; i++ ){
if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
- unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2;
+ unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2;
bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
return isEntailed2( n[ch], subs, subsRep, hasSubs, reqPol, qy );
}
}
bool TermDb::isAssoc( Kind k ) {
- return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+ return k==PLUS || k==MULT || k==AND || k==OR ||
k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT ||
k==STRING_CONCAT;
}
bool TermDb::isComm( Kind k ) {
- return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+ return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR ||
k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
}
bool TermDb::isBoolConnective( Kind k ) {
- return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT || k==SEP_STAR;
+ return k==OR || k==AND || k==EQUAL || k==ITE || k==FORALL || k==NOT || k==SEP_STAR;
+}
+
+bool TermDb::isBoolConnectiveTerm( TNode n ) {
+ return isBoolConnective( n.getKind() ) &&
+ ( n.getKind()!=EQUAL || n[0].getType().isBoolean() ) &&
+ ( n.getKind()!=ITE || n.getType().isBoolean() );
}
void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
}
Node TermDb::getFunDefHead( Node q ) {
- //&& ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF &&
+ //&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF &&
if( q.getKind()==FORALL && q.getNumChildren()==3 ){
for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
Node TermDb::getFunDefBody( Node q ) {
Node h = getFunDefHead( q );
if( !h.isNull() ){
- if( q[1].getKind()==EQUAL || q[1].getKind()==IFF ){
+ if( q[1].getKind()==EQUAL ){
if( q[1][0]==h ){
return q[1][1];
}else if( q[1][1]==h ){
return arg==1;
}
}else if( n==getTypeMaxValue( tn ) ){
- if( ik==IFF || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){
+ if( ik==EQUAL || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){
return true;
}
}
}
Node TermDbSygus::expandBuiltinTerm( Node t ){
- if( t.getKind()==EQUAL && ( t[0].getType().isInteger() || t[0].getType().isReal() ) ){
- return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ),
- NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) );
+ if( t.getKind()==EQUAL ){
+ if( t[0].getType().isReal() ){
+ return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ),
+ NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) );
+ }else if( t[0].getType().isBoolean() ){
+ return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
+ NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
+ }
}else if( t.getKind()==ITE && t.getType().isBoolean() ){
return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) );
- }else if( t.getKind()==IFF ){
- return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
- NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
}
return Node::null();
}
Assert( dt.isSygus() );
d_eval_args[n[0]].push_back( std::vector< Node >() );
for( unsigned j=1; j<n.getNumChildren(); j++ ){
- if( var_list[j-1].getType().isBoolean() ){
- //TODO: remove this case when boolean term conversion is eliminated
- Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
- d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) );
- }else{
+ //if( var_list[j-1].getType().isBoolean() ){
+ // //TODO: remove this case when boolean term conversion is eliminated
+ // Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+ // d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) );
+ //}else{
d_eval_args[n[0]].back().push_back( n[j] );
- }
+ //}
}
Node a = getAnchor( n[0] );
d_subterms[a][n[0]] = true;
for( unsigned i=start; i<it->second.size(); i++ ){
Assert( vars.size()==it->second[i].size() );
Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
- Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm );
+ Node lem = NodeManager::currentNM()->mkNode(EQUAL, d_evals[n][i], sBTerm );
lem = NodeManager::currentNM()->mkNode( OR, antec, lem );
Trace("sygus-eager") << "Lemma : " << lem << std::endl;
lems.push_back( lem );
static bool isComm( Kind k );
/** is bool connective */
static bool isBoolConnective( Kind k );
+ /** is bool connective term */
+ static bool isBoolConnectiveTerm( TNode n );
//for sygus
private:
Assert( isRelationalTrigger( n ) );
for( unsigned i=0; i<2; i++) {
if( isUsableEqTerms( q, n[i], n[1-i] ) ){
- if( i==1 && ( n.getKind()==EQUAL || n.getKind()==IFF ) && !quantifiers::TermDb::hasInstConstAttr(n[0]) ){
+ if( i==1 && n.getKind()==EQUAL && !quantifiers::TermDb::hasInstConstAttr(n[0]) ){
return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] );
}else{
return n;
n = n[0];
}
if( n.getKind()==INST_CONSTANT ){
- return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
+ return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
}else if( isRelationalTrigger( n ) ){
Node rtr = getIsUsableEq( q, n );
if( rtr.isNull() && n[0].getType().isReal() ){
}else{
Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermDb::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
if( isUsableAtomicTrigger( n, q ) ){
- return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
+ return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
}
}
return Node::null();
}
bool Trigger::isRelationalTriggerKind( Kind k ) {
- return k==EQUAL || k==IFF || k==GEQ;
+ return k==EQUAL || k==GEQ;
}
bool Trigger::isCbqiKind( Kind k ) {
bool Trigger::isSimpleTrigger( Node n ){
Node t = n.getKind()==NOT ? n[0] : n;
- if( t.getKind()==IFF || t.getKind()==EQUAL ){
+ if( t.getKind()==EQUAL ){
if( !quantifiers::TermDb::hasInstConstAttr( t[1] ) ){
t = t[0];
}
Assert( nu.getKind()!=NOT );
Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
Node reqEq;
- if( nu.getKind()==IFF || nu.getKind()==EQUAL ){
+ if( nu.getKind()==EQUAL ){
if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){
if( hasPol ){
reqEq = nu[1];
bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){
//Assert( !areEqual( n1, n2 ) );
//Assert( !areDisequal( n1, n2 ) );
- Kind knd = n1.getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
- Node fm = NodeManager::currentNM()->mkNode( knd, n1, n2 );
+ Node fm = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 );
return addSplit( fm );
}
Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
#ifdef CVC4_ASSERTIONS
- bool isEquality = node.getKind() == kind::EQUAL;
+ bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
if(s_rewriteStack == NULL) {
s_rewriteStack = new std::hash_set<Node, NodeHashFunction>();
// Do the work
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
- if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+ if (atom.getKind() == kind::EQUAL) {
d_equalityEngine.explainEquality( atom[0], atom[1], polarity, assumptions, NULL );
} else {
d_equalityEngine.explainPredicate( atom, polarity, assumptions );
}
Node nil = getNilRef( it->first );
Node vnil = d_valuation.getModel()->getRepresentative( nil );
- m_neq = NodeManager::currentNM()->mkNode( nil.getType().isBoolean() ? kind::IFF : kind::EQUAL, nil, vnil );
+ m_neq = NodeManager::currentNM()->mkNode( kind::EQUAL, nil, vnil );
Trace("sep-model") << "sep.nil = " << vnil << std::endl;
Trace("sep-model") << std::endl;
if( sep_children.empty() ){
d_out->requirePhase( lit, true );
d_neg_guards.push_back( lit );
d_guard_to_assertion[lit] = s_atom;
- //Node lem = NodeManager::currentNM()->mkNode( kind::IFF, lit, conc );
+ //Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, lit, conc );
Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit.negate(), conc );
Trace("sep-lemma") << "Sep::Lemma : (neg) reduction : " << lem << std::endl;
d_out->lemma( lem );
void TheorySep::conflict(TNode a, TNode b) {
Trace("sep-conflict") << "Sep::conflict : " << a << " " << b << std::endl;
- Node conflictNode;
- if (a.getKind() == kind::CONST_BOOLEAN) {
- conflictNode = explain(a.iffNode(b));
- } else {
- conflictNode = explain(a.eqNode(b));
- }
+ Node conflictNode = explain(a.eqNode(b));
d_conflict = true;
d_out->conflict( conflictNode );
}
Node e = d_type_references_card[tn][r];
//ensure that it is distinct from all other references so far
for( unsigned j=0; j<d_type_references_all[tn].size(); j++ ){
- Node eq = NodeManager::currentNM()->mkNode( e.getType().isBoolean() ? kind::IFF : kind::EQUAL, e, d_type_references_all[tn][j] );
+ Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, e, d_type_references_all[tn][j] );
d_out->lemma( eq.negate() );
}
d_type_references_all[tn].push_back( e );
std::map< Node, Node >::iterator it = pto_model.find( vr );
if( it!=pto_model.end() ){
if( n[1]!=it->second ){
- children.push_back( NodeManager::currentNM()->mkNode( n[1].getType().isBoolean() ? kind::IFF : kind::EQUAL, n[1], it->second ) );
+ children.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[1], it->second ) );
}
}else{
Trace("sep-inst-debug") << "Data for " << vr << " was not specified, do not add condition." << std::endl;
}
break;
}
- case kind::EQUAL:
- case kind::IFF: {
+ case kind::EQUAL: {
if(node[0] == node[1]) {
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
}
}
if( x!=itnm2->second[xr][0] ){
Assert( d_equalityEngine.areEqual( x, itnm2->second[xr][0] ) );
- exp.push_back( NodeManager::currentNM()->mkNode( x.getType().isBoolean() ? kind::IFF : kind::EQUAL, x, itnm2->second[xr][0] ) );
+ exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, x, itnm2->second[xr][0] ) );
}
valid = true;
}
Node x = NodeManager::currentNM()->mkSkolem("sde_", elementType);
Node mem1 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[0] );
Node mem2 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[1] );
- Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq, NodeManager::currentNM()->mkNode( kind::IFF, mem1, mem2 ).negate() );
+ Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq, NodeManager::currentNM()->mkNode( kind::EQUAL, mem1, mem2 ).negate() );
lem = Rewriter::rewrite( lem );
assertInference( lem, d_emp_exp, lemmas, "diseq", 1 );
flushLemmas( lemmas );
void TheorySetsPrivate::conflict(TNode a, TNode b)
{
- if (a.getKind() == kind::CONST_BOOLEAN) {
- d_conflictNode = explain(a.iffNode(b));
- } else {
- d_conflictNode = explain(a.eqNode(b));
- }
+ d_conflictNode = explain(a.eqNode(b));
d_external.d_out->conflict(d_conflictNode);
Debug("sets") << "[sets] conflict: " << a << " iff " << b
<< ", explaination " << d_conflictNode << std::endl;
TNode atom = polarity ? literal : literal[0];
std::vector<TNode> assumptions;
- if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+ if(atom.getKind() == kind::EQUAL) {
d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
} else if(atom.getKind() == kind::MEMBER) {
if( !d_equalityEngine.hasTerm(atom)) {
}
Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
tuple_reduct = NodeManager::currentNM()->mkNode(kind::MEMBER,tuple_reduct, n[1]);
- Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::IFF, n, tuple_reduct);
+ Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::EQUAL, n, tuple_reduct);
sendLemma(tuple_reduction_lemma, d_trueNode, "tuple-reduction");
d_symbolic_tuples.insert(n);
}
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
- if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+ if(atom.getKind() == kind::EQUAL) {
d_eqEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
} else if(atom.getKind() == kind::MEMBER) {
if( !d_eqEngine->hasTerm(atom)) {
B) );
}//kind::SUBSET
- case kind::EQUAL:
- case kind::IFF: {
+ case kind::EQUAL: {
//rewrite: t = t with true (t term)
//rewrite: c = c' with c different from c' false (c, c' constants)
//otherwise: sort them
return RewriteResponse(REWRITE_DONE, newNode);
}
break;
- }//kind::IFF
+ }
case kind::SETMINUS: {
if(node[0] == node[1]) {
Trace("sort-inference-debug") << "...Process " << n << std::endl;
int retType;
- if( n.getKind()==kind::EQUAL ){
+ if( n.getKind()==kind::EQUAL && !n[0].getType().isBoolean() ){
Trace("sort-inference-debug") << "For equality " << n << ", set equal types from : " << n[0].getType() << " " << n[1].getType() << std::endl;
//if original types are mixed (e.g. Int/Real), don't commit type equality in either direction
if( n[0].getType()!=n[1].getType() ){
TNode atom = polarity ? literal : literal[0];
unsigned ps = assumptions.size();
std::vector< TNode > tassumptions;
- if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+ if (atom.getKind() == kind::EQUAL) {
if( atom[0]!=atom[1] ){
Assert( hasTerm( atom[0] ) );
Assert( hasTerm( atom[1] ) );
std::vector< Node > new_nodes;
Node res = d_preproc.simplify( n, new_nodes );
Assert( res!=n );
- new_nodes.push_back( NodeManager::currentNM()->mkNode( res.getType().isBoolean() ? kind::IFF : kind::EQUAL, res, n ) );
+ new_nodes.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, res, n ) );
Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
nnlem = Rewriter::rewrite( nnlem );
Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
Debug("strings-conflict") << "Making conflict..." << std::endl;
d_conflict = true;
Node conflictNode;
- if (a.getKind() == kind::CONST_BOOLEAN) {
- conflictNode = explain( a.iffNode(b) );
- } else {
- conflictNode = explain( a.eqNode(b) );
- }
+ conflictNode = explain( a.eqNode(b) );
Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
d_out->conflict( conflictNode );
}
new_nodes.push_back(lencond);
}
- Node lem = NodeManager::currentNM()->mkNode(kind::IFF, nonneg.negate(),
+ Node lem = NodeManager::currentNM()->mkNode(kind::EQUAL, nonneg.negate(),
pret.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero)
);
new_nodes.push_back(lem);
str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
pret.eqNode(negone));
new_nodes.push_back(lem);
- /*lem = NodeManager::currentNM()->mkNode(kind::IFF,
+ /*lem = NodeManager::currentNM()->mkNode(kind::EQUAL,
t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))),
t.eqNode(d_zero));
new_nodes.push_back(lem);*/
for(unsigned i=0; i<=9; i++) {
chtmp[0] = i + '0';
std::string stmp(chtmp);
- c3cc = NodeManager::currentNM()->mkNode(kind::IFF,
+ c3cc = NodeManager::currentNM()->mkNode(kind::EQUAL,
ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(i))),
sx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(stmp))));
vec_c3b.push_back(c3cc);
switch(mode) {
case THEORY_OF_TYPE_BASED:
// Constants, variables, 0-ary constructors
- if (node.isVar() || node.isConst()) {
+ if (node.isVar()) {
+ if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
+ tid = THEORY_UF;
+ }else{
+ tid = Theory::theoryOf(node.getType());
+ }
+ }else if (node.isConst()) {
tid = Theory::theoryOf(node.getType());
} else if (node.getKind() == kind::EQUAL) {
// Equality is owned by the theory that owns the domain
// We treat the variables as uninterpreted
tid = s_uninterpretedSortOwner;
} else {
- // Except for the Boolean ones, which we just ignore anyhow
- tid = theory::THEORY_BOOL;
+ if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
+ //Boolean vars go to UF
+ tid = THEORY_UF;
+ }else{
+ // Except for the Boolean ones
+ tid = THEORY_BOOL;
+ }
}
} else if (node.isConst()) {
// Constants go to the theory of the type
nred.push_back( n );
}else{
if( !nr.isNull() && n!=nr ){
- Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? kind::IFF : kind::EQUAL, n, nr );
+ Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr );
if( sendLemma( lem, true ) ){
Trace("extt-lemma") << "ExtTheory : Reduction lemma : " << lem << std::endl;
addedLemma = true;
}
break;
- case kind::IFF:
- if (!negated) {
- registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1].negate()), originalLemma, false, theoryId);
- registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId);
- } else {
- registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1]), originalLemma, false, theoryId);
- registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId);
+ case kind::EQUAL:
+ if( nnLemma[0].getType().isBoolean() ){
+ if (!negated) {
+ registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1].negate()), originalLemma, false, theoryId);
+ registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId);
+ } else {
+ registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1]), originalLemma, false, theoryId);
+ registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId);
+ }
}
break;
TheoryEngine::TheoryEngine(context::Context* context,
context::UserContext* userContext,
- RemoveITE& iteRemover,
+ RemoveTermFormulas& iteRemover,
const LogicInfo& logicInfo,
LemmaChannels* channels)
: d_propEngine(NULL),
d_propagatedLiterals(context),
d_propagatedLiteralsIndex(context, 0),
d_atomRequests(context),
- d_iteRemover(iteRemover),
+ d_tform_remover(iteRemover),
d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
d_true(),
d_false(),
ProofManager::currentPM()->initTheoryProofEngine();
#endif
- d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());
+ d_iteUtilities = new ITEUtilities(d_tform_remover.getContainsVisitor());
smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
}
Node ppNode = preprocess ? this->preprocess(node) : Node(node);
// Remove the ITEs
+ Debug("ite") << "Remove ITE from " << ppNode << std::endl;
additionalLemmas.push_back(ppNode);
- d_iteRemover.run(additionalLemmas, iteSkolemMap);
+ d_tform_remover.run(additionalLemmas, iteSkolemMap);
+ Debug("ite") << "..done " << additionalLemmas[0] << std::endl;
additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
if(Debug.isOn("lemma-ites")) {
Node TheoryEngine::ppSimpITE(TNode assertion)
{
- if (!d_iteRemover.containsTermITE(assertion)) {
+ if (!d_tform_remover.containsTermITE(assertion)) {
return assertion;
} else {
Node result = d_iteUtilities->simpITE(assertion);
Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl;
d_iteUtilities->clear();
Rewriter::clearCaches();
- d_iteRemover.garbageCollect();
+ d_tform_remover.garbageCollect();
nm->reclaimZombiesUntil(options::zombieHuntThreshold());
Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl;
}
if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH)
&& !options::incrementalSolving() ){
if(!simpDidALotOfWork){
- ContainsTermITEVisitor& contains = *d_iteRemover.getContainsVisitor();
+ ContainsTermITEVisitor& contains = *d_tform_remover.getContainsVisitor();
arith::ArithIteUtils aiteu(contains, d_userContext, getModel());
bool anyItes = false;
for(size_t i = 0; i < assertions.size(); ++i){
}
Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl;
- Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially");
+ Assert( explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially");
// Mark the explanation
NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp);
explanationVector.push_back(newExplain);
}/* CVC4::theory namespace */
class DecisionEngine;
-class RemoveITE;
+class RemoveTermFormulas;
class UnconstrainedSimplifier;
/**
/** Enusre that the given atoms are send to the given theory */
void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
- RemoveITE& d_iteRemover;
+ RemoveTermFormulas& d_tform_remover;
/** sort inference module */
SortInference d_sortInfer;
/** Constructs a theory engine */
TheoryEngine(context::Context* context, context::UserContext* userContext,
- RemoveITE& iteRemover, const LogicInfo& logic,
+ RemoveTermFormulas& iteRemover, const LogicInfo& logic,
LemmaChannels* channels);
/** Destroys a theory engine */
theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
- RemoveITE* getIteRemover() { return &d_iteRemover; }
+ RemoveTermFormulas* getTermFormulaRemover() { return &d_tform_remover; }
SortInference* getSortInference() { return &d_sortInfer; }
d_isConstant.push_back(false);
// No terms to evaluate by defaul
d_subtermsToEvaluate.push_back(0);
- // Mark Boolean nodes
- d_isBoolean.push_back(false);
+ // Mark equality nodes
+ d_isEquality.push_back(false);
// Mark the node as internal by default
d_isInternal.push_back(true);
// Add the equality node to the nodes
d_isConstant[result] = !isOperator && t.isConst();
}
- if (t.getType().isBoolean()) {
+ if (t.getKind() == kind::EQUAL) {
// We set this here as this only applies to actual terms, not the
// intermediate application terms
- d_isBoolean[result] = true;
+ d_isEquality[result] = true;
} else if (d_constantsAreTriggers && d_isConstant[result]) {
// Non-Boolean constants are trigger terms for all tags
EqualityNodeId tId = getNodeId(t);
// Update class2 table lookup and information if not a boolean
// since booleans can't be in an application
- if (!d_isBoolean[class2Id]) {
+ if (!d_isEquality[class2Id]) {
Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl;
do {
// Get the current node
d_nodeIndividualTrigger.resize(d_nodesCount);
d_isConstant.resize(d_nodesCount);
d_subtermsToEvaluate.resize(d_nodesCount);
- d_isBoolean.resize(d_nodesCount);
+ d_isEquality.resize(d_nodesCount);
d_isInternal.resize(d_nodesCount);
d_equalityGraph.resize(d_nodesCount);
d_equalityNodes.resize(d_nodesCount);
} else {
eqp->d_id = MERGED_THROUGH_TRANS;
eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
- eqp->d_node = NodeManager::currentNM()->mkNode(d_nodes[t1Id].getType().isBoolean() ? kind::IFF : kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]);
+ eqp->d_node = NodeManager::currentNM()->mkNode(kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]);
}
eqp->debug_print("pf::ee", 1);
/**
* Map from ids to whether they are Boolean.
*/
- std::vector<bool> d_isBoolean;
+ std::vector<bool> d_isEquality;
/**
* Map from ids to whether the nods is internal. An internal node is a node
typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule
+variable BOOLEAN_TERM_VARIABLE "Boolean term variable"
+
operator CARDINALITY_CONSTRAINT 2 "cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S"
typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule
} else {
if( (*i).getKind() == kind::OR ) {
kids.push_back(normInternal(*i, level));
- } else if((*i).getKind() == kind::IFF ||
- (*i).getKind() == kind::EQUAL) {
+ } else if((*i).getKind() == kind::EQUAL) {
kids.push_back(normInternal(*i, level));
if((*i)[0].isVar() ||
(*i)[1].isVar()) {
first = false;
matchingTerm = TNode::null();
kids.push_back(normInternal(*i, level + 1));
- } else if((*i).getKind() == kind::IFF ||
- (*i).getKind() == kind::EQUAL) {
+ } else if((*i).getKind() == kind::EQUAL) {
kids.push_back(normInternal(*i, level + 1));
if((*i)[0].isVar() ||
(*i)[1].isVar()) {
sort(kids.begin(), kids.end());
return result = NodeManager::currentNM()->mkNode(k, kids);
}
-
- case kind::IFF:
+
case kind::EQUAL:
if(n[0].isVar() ||
n[1].isVar()) {
}
}
-
- if (d_thss != NULL && ! d_conflict) {
- d_thss->check(level);
- if( d_thss->isConflict() ){
- d_conflict = true;
+ if(! d_conflict ){
+ if (d_thss != NULL) {
+ d_thss->check(level);
+ if( d_thss->isConflict() ){
+ d_conflict = true;
+ }
}
}
-
}/* TheoryUF::check() */
void TheoryUF::preRegisterTerm(TNode node) {
// Do the work
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
- if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+ if (atom.getKind() == kind::EQUAL) {
d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf);
} else {
d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf);
if(n.getKind() == kind::OR && n.getNumChildren() == 2 &&
n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 &&
n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 &&
- (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) &&
- (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) &&
- (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) &&
- (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) {
+ (n[0][0].getKind() == kind::EQUAL) &&
+ (n[0][1].getKind() == kind::EQUAL) &&
+ (n[1][0].getKind() == kind::EQUAL) &&
+ (n[1][1].getKind() == kind::EQUAL)) {
// now we have (a = b && c = d) || (e = f && g = h)
Debug("diamonds") << "has form of a diamond!" << endl;
(a == h && d == e) ) {
// learn: n implies a == d
Debug("diamonds") << "+ C holds" << endl;
- Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d);
+ Node newEquality = a.eqNode(d);
Debug("diamonds") << " ==> " << newEquality << endl;
learned << n.impNode(newEquality);
} else {
void TheoryUF::conflict(TNode a, TNode b) {
eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL;
-
- if (a.getKind() == kind::CONST_BOOLEAN) {
- d_conflictNode = explain(a.iffNode(b),pf);
- } else {
- d_conflictNode = explain(a.eqNode(b),pf);
- }
+ d_conflictNode = explain(a.eqNode(b),pf);
ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
d_out->conflict(d_conflictNode, puf);
d_conflict = true;
}
void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
- Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+ Debug("uf-notify") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_uf.conflict(t1, t2);
}
void eqNotifyNewClass(TNode t) {
- Debug("uf") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
+ Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl;
d_uf.eqNotifyNewClass(t);
}
void eqNotifyPreMerge(TNode t1, TNode t2) {
- Debug("uf") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
+ Debug("uf-notify") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_uf.eqNotifyPreMerge(t1, t2);
}
void eqNotifyPostMerge(TNode t1, TNode t2) {
- Debug("uf") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
+ Debug("uf-notify") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_uf.eqNotifyPostMerge(t1, t2);
}
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
- Debug("uf") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
+ Debug("uf-notify") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
d_uf.eqNotifyDisequal(t1, t2, reason);
}
public:
static RewriteResponse postRewrite(TNode node) {
- if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) {
+ if(node.getKind() == kind::EQUAL) {
if(node[0] == node[1]) {
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
} else if(node[0].isConst() && node[1].isConst()) {
}
static RewriteResponse preRewrite(TNode node) {
- if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) {
+ if(node.getKind() == kind::EQUAL) {
if(node[0] == node[1]) {
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
} else if(node[0].isConst() && node[1].isConst()) {
int bi = d_regions_map[b];
if( !d_regions[ai]->isDisequal( a, b, ai==bi ) ){
Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl;
- //if( reason.getKind()!=NOT || ( reason[0].getKind()!=EQUAL && reason[0].getKind()!=IFF ) ||
+ //if( reason.getKind()!=NOT || reason[0].getKind()!=EQUAL ||
// a!=reason[0][0] || b!=reason[0][1] ){
// Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl;
//}
//otherwise, make equal via lemma
if( d_card_assertions_eqv_lemma.find( lit )==d_card_assertions_eqv_lemma.end() ){
Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
- Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << lit.iffNode( eqv_lit ) << std::endl;
- getOutputChannel().lemma( lit.iffNode( eqv_lit ) );
+ eqv_lit = lit.eqNode( eqv_lit );
+ Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl;
+ getOutputChannel().lemma( eqv_lit );
d_card_assertions_eqv_lemma[lit] = true;
}
}
parent = d_visitedOnce[current];
if (!parent.isNull()) {
swap = isSigned = strict = false;
+ bool checkParent = false;
switch (parent.getKind()) {
// If-then-else operator - any two unconstrained children makes the parent unconstrained
if (card.isFinite() && !card.isLargeFinite() && card.getFiniteCardinality() == 2) {
// Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result
// is unconstrained
- Node test;
- if (parent.getType().isBoolean()) {
- test = Rewriter::rewrite(parent[1].iffNode(parent[2]));
- }
- else {
- test = Rewriter::rewrite(parent[1].eqNode(parent[2]));
- }
+ Node test = Rewriter::rewrite(parent[1].eqNode(parent[2]));
if (test == NodeManager::currentNM()->mkConst<bool>(false)) {
++d_numUnconstrainedElim;
if (currentSub.isNull()) {
break;
}
}
+ if( parent[0].getType().isBoolean() ){
+ checkParent = true;
+ break;
+ }
case kind::BITVECTOR_COMP:
case kind::LT:
case kind::LEQ:
}
}
if (allUnconstrained) {
- if (d_unconstrained.find(parent) == d_unconstrained.end() &&
- !d_substitutions.hasSubstitution(parent)) {
- ++d_numUnconstrainedElim;
- if (currentSub.isNull()) {
- currentSub = current;
- }
- current = parent;
- }
- else {
- currentSub = Node();
- }
+ checkParent = true;
}
}
break;
}
}
if (allUnconstrained && allDifferent) {
- if (d_unconstrained.find(parent) == d_unconstrained.end() &&
- !d_substitutions.hasSubstitution(parent)) {
- ++d_numUnconstrainedElim;
- if (currentSub.isNull()) {
- currentSub = current;
- }
- current = parent;
- }
- else {
- currentSub = Node();
- }
+ checkParent = true;
}
break;
}
!parent.getType().isInteger()) {
break;
}
- case kind::IFF:
case kind::XOR:
case kind::BITVECTOR_XOR:
case kind::BITVECTOR_XNOR:
case kind::BITVECTOR_PLUS:
case kind::BITVECTOR_SUB:
- if (d_unconstrained.find(parent) == d_unconstrained.end() &&
- !d_substitutions.hasSubstitution(parent)) {
- ++d_numUnconstrainedElim;
- if (currentSub.isNull()) {
- currentSub = current;
- }
- current = parent;
- }
- else {
- currentSub = Node();
- }
+ checkParent = true;
break;
// Multiplication/division: must be non-integer and other operand must be non-zero
if (done) {
break;
}
- if (d_unconstrained.find(parent) == d_unconstrained.end() &&
- !d_substitutions.hasSubstitution(parent)) {
- ++d_numUnconstrainedElim;
- if (currentSub.isNull()) {
- currentSub = current;
- }
- current = parent;
- }
- else {
- currentSub = Node();
- }
+ checkParent = true;
break;
}
default:
break;
}
+ if( checkParent ){
+ //run for various cases from above
+ if (d_unconstrained.find(parent) == d_unconstrained.end() &&
+ !d_substitutions.hasSubstitution(parent)) {
+ ++d_numUnconstrainedElim;
+ if (currentSub.isNull()) {
+ currentSub = current;
+ }
+ current = parent;
+ }
+ else {
+ currentSub = Node();
+ }
+ }
if (current == parent && d_visited[parent] == 1) {
d_unconstrained.insert(parent);
continue;
bug595.cvc \
bug596.cvc \
bug596b.cvc \
- bug605.cvc
+ bug605.cvc \
+ bt-test-00.smt2 \
+ bt-test-01.smt2
#bug590.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
constarr2.cvc \
constarr3.cvc \
parsing_ringer.cvc \
- bug637.delta.smt2
+ bug637.delta.smt2 \
+ bool-array.smt2
EXTRA_DIST = $(TESTS)
--- /dev/null
+; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic QF_AX)
+(set-info :status unsat)
+
+(declare-fun a () (Array Bool Bool))
+(declare-fun b () (Array Bool Bool))
+
+(assert (not (= (select a (= a b)) (select a (not (= a b))))))
+(assert (= (select a true) (select a false)))
+
+(check-sat)
+
--- /dev/null
+; COMMAND-LINE: --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_UF)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+
+(declare-fun f (Bool) Bool)
+(declare-fun g (Bool) Bool)
+(declare-fun h (Bool) Bool)
+
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(declare-fun z () Bool)
+
+(assert (not (= (f x) (f y))))
+(assert (not (= (g y) (g z))))
+(assert (not (= (h z) (h x))))
+
+(check-sat)
+
+(exit)
--- /dev/null
+; COMMAND-LINE: --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_UF)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+
+(declare-fun x0 () Bool)
+(declare-fun y0 () Bool)
+(declare-fun z0 () Bool)
+
+(assert (or x0 y0))
+(assert (or (not y0) z0))
+
+(declare-fun x1 () Bool)
+(declare-fun y1 () Bool)
+
+(assert x1)
+(assert y1)
+
+(declare-fun f (Bool) Bool)
+
+(assert (not (= (f (or x0 z0)) (f (and x1 y1)))))
+
+(check-sat)
+
+(exit)
+; COMMAND-LINE: --no-check-proofs
; EXPECT: unsat
(set-logic QF_UF)
-(set-info :status sat)
+(set-info :status unsat)
(set-option :produce-models true)
(declare-fun f (Bool) Bool)
(declare-fun x () Bool)
coda_simp_model.smt2 \
Test1-tup-mp.cvc \
dt-param-card4-unsat.smt2 \
- dt-param-card4-bool-sat.smt2
+ dt-param-card4-bool-sat.smt2 \
+ bug604.smt2 \
+ bug597-rbt.smt2 \
+ example-dailler-min.smt2
FAILING_TESTS = \
datatype-dump.cvc
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+; Tree type
+(declare-datatypes () ((Tree (node (data Int) (color Bool) (left Tree) (right Tree)) (nil))))
+
+; content function
+(declare-fun size (Tree) Int)
+(assert (= (size nil) 0))
+
+
+(check-sat)
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () ( (PairIntInt (pair (firstPairIntInt Int)
+(secondPairIntInt Int)) ) ))
+(declare-fun /ArrayIntOfPair () (Array Int PairIntInt))
+(declare-datatypes () ( (SequenceABC (sequenceABC (a Int) (b Bool) (c Int)) )
+))
+(declare-fun /ArrayIntOfSequenceABC () (Array Int SequenceABC))
+(check-sat)
--- /dev/null
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes () ((D (C (R Bool)))))
+(declare-fun a () (Array Int D))
+(declare-fun P ((Array Int D)) Bool)
+(assert (P a))
+(check-sat)
memory_model-R_cpp-dd.cvc \
bug764.smt2 \
ko-bound-set.cvc \
- cons-sets-bounds.smt2
+ cons-sets-bounds.smt2 \
+ bug651.smt2 \
+ bug652.smt2
EXTRA_DIST = $(TESTS)
--- /dev/null
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+(set-logic UFDTSLIA)
+(set-info :smt-lib-version 2.5)
+(set-option :produce-models true)
+
+(declare-datatypes () (
+ (Conditional_Int (Conditional_Int$CAbsent_Int) (Conditional_Int$CPresent_Int (Conditional_Int$CPresent_Int$value Int)))
+ (Conditional_T_titleType (Conditional_T_titleType$CAbsent_T_titleType) (Conditional_T_titleType$CPresent_T_titleType (Conditional_T_titleType$CPresent_T_titleType$value T_titleType)))
+ (Conditional_boolean (Conditional_boolean$CAbsent_boolean) (Conditional_boolean$CPresent_boolean (Conditional_boolean$CPresent_boolean$value Bool)))
+ (Conditional_string (Conditional_string$CAbsent_string) (Conditional_string$CPresent_string (Conditional_string$CPresent_string$value String)))
+ (Double (Double$CINF) (Double$CNINF) (Double$CNaN) (Double$CValue (Double$CValue$value Int)))
+ (List_T_titleType (List_T_titleType$CNil_T_titleType) (List_T_titleType$Cstr_T_titleType (List_T_titleType$Cstr_T_titleType$head T_titleType) (List_T_titleType$Cstr_T_titleType$tail List_T_titleType)))
+ (List_boolean (List_boolean$CNil_boolean) (List_boolean$Cstr_boolean (List_boolean$Cstr_boolean$head Bool) (List_boolean$Cstr_boolean$tail List_boolean)))
+ (List_string (List_string$CNil_string) (List_string$Cstr_string (List_string$Cstr_string$head String) (List_string$Cstr_string$tail List_string)))
+ (T_titleType (T_titleType$C_T_titleType (T_titleType$C_T_titleType$base String)))
+) )
+
+(define-fun f1361$isValid_string((x String)) Bool true)
+(define-fun f5131$isValid_T_titleType((x T_titleType)) Bool (and (f1361$isValid_string (T_titleType$C_T_titleType$base x)) (<= (str.len (T_titleType$C_T_titleType$base x)) 80)))
+(define-funs-rec
+ (
+ (f5242$isValidElementsList_T_titleType((x List_T_titleType)) Bool)
+ )
+ (
+ (=> (is-List_T_titleType$Cstr_T_titleType x) (and (f5131$isValid_T_titleType (List_T_titleType$Cstr_T_titleType$head x)) (f5242$isValidElementsList_T_titleType (List_T_titleType$Cstr_T_titleType$tail x))))
+ )
+)
+(define-fun f1348$isValid_boolean((x Bool)) Bool true)
+(define-funs-rec
+ (
+ (f4169$isValidElementsList_boolean((x List_boolean)) Bool)
+ )
+ (
+ (=> (is-List_boolean$Cstr_boolean x) (and (f1348$isValid_boolean (List_boolean$Cstr_boolean$head x)) (f4169$isValidElementsList_boolean (List_boolean$Cstr_boolean$tail x))))
+ )
+)
+
+
+(declare-const title T_titleType)
+(check-sat)
+
+
--- /dev/null
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+(set-logic UFDTSLIA)
+(set-info :smt-lib-version 2.5)
+(set-option :produce-models true)
+
+(declare-datatypes () (
+ (List_boolean (List_boolean$CNil_boolean) (List_boolean$Cstr_boolean (List_boolean$Cstr_boolean$head Bool) (List_boolean$Cstr_boolean$tail List_boolean)))
+) )
+
+(define-funs-rec
+ (
+ (f4208$lengthList_boolean((x List_boolean)) Int)
+ )
+ (
+ (ite (is-List_boolean$CNil_boolean x) 0 (+ 1 (f4208$lengthList_boolean (List_boolean$Cstr_boolean$tail x))))
+ )
+)
+
+
+(declare-const boolean Bool)
+(check-sat)
inc-double-u.smt2 \
fmf-fun-dbu.smt2 \
inc-define.smt2 \
- bug765.smt2
+ bug765.smt2 \
+ bug691.smt2 \
+ bug694-Unapply1.scala-0.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
--- /dev/null
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+(set-logic UFDTSLIA)
+(set-info :smt-lib-version 2.5)
+
+(declare-datatypes () (
+ (Response (Response$Response (Response$Response$success Bool)))
+ ) )
+
+
+(push 1)
+(declare-fun $BLout$3248$0$1$() Response)
+(assert (= $BLout$3248$0$1$ (Response$Response true)))
+(check-sat)
+(pop 1)
+
+(push 1)
+(declare-fun $BLout$3248$2$1$() Response)
+(assert (= $BLout$3248$2$1$ (Response$Response true)))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun start!1 () Bool)
+
+(assert start!1)
+
+(declare-fun b!15 () Bool)
+
+(declare-fun e!22 () Bool)
+
+(declare-fun error_value!0 () Bool)
+
+(assert (=> b!15 (= e!22 error_value!0)))
+
+(declare-fun b!16 () Bool)
+
+(declare-fun e!20 () Bool)
+
+(assert (=> b!16 (= e!20 e!22)))
+
+(declare-fun b!20 () Bool)
+
+(declare-datatypes () ( (Option!3 (None!1) (Some!1 (v!71 tuple2!0))) (tuple2!0 (tuple2!1 (_1!0 Unit!0) (_2!0 Bool))) (Unit!0 (Unit!1)) ))
+
+(declare-fun lt!7 () Option!3)
+
+(declare-fun Unit!2 () Unit!0)
+
+(assert (=> b!16 (= b!20 (ite (is-Some!1 lt!7) (= (_1!0 (v!71 lt!7)) Unit!2) false))))
+
+(assert (=> b!16 (or (not b!20) (not b!15))))
+
+(assert (=> b!16 (or b!20 b!15)))
+
+(declare-datatypes () ( (tuple3!0 (tuple3!1 (_1!1 (_ BitVec 32)) (_2!1 Bool) (_3!0 Unit!0))) ))
+
+(declare-fun unapply!2 (tuple3!0) Option!3)
+
+(declare-fun Unit!3 () Unit!0)
+
+(assert (=> b!16 (= lt!7 (unapply!2 (tuple3!1 #x0000002A false Unit!3)))))
+
+(declare-fun b!17 () Bool)
+
+(declare-fun e!21 () Bool)
+
+(assert (=> b!17 e!21))
+
+(declare-fun b!18 () Bool)
+
+(declare-fun Unit!4 () Unit!0)
+
+(assert (=> b!18 (= e!20 (_2!0 (v!71 (unapply!2 (tuple3!1 #x0000002A false Unit!4)))))))
+
+(declare-fun lt!6 () Bool)
+
+(assert (=> start!1 (not lt!6)))
+
+(assert (=> start!1 (= lt!6 e!20)))
+
+(assert (=> start!1 (= b!18 e!21)))
+
+(assert (=> start!1 (or (not b!18) (not b!16))))
+
+(assert (=> start!1 (or b!18 b!16)))
+
+(declare-fun b!19 () Bool)
+
+(assert (=> (and start!1 (not b!19)) (not e!21)))
+
+(declare-fun lt!8 () Option!3)
+
+(assert (=> start!1 (= b!19 (ite (is-Some!1 lt!8) true false))))
+
+(declare-fun Unit!5 () Unit!0)
+
+(assert (=> start!1 (= lt!8 (unapply!2 (tuple3!1 #x0000002A false Unit!5)))))
+
+(assert (=> (and b!19 (not b!17)) (not e!21)))
+
+(declare-fun Unit!6 () Unit!0)
+
+(assert (=> b!19 (= b!17 (_2!0 (v!71 (unapply!2 (tuple3!1 #x0000002A false Unit!6)))))))
+
+(declare-fun Unit!7 () Unit!0)
+
+(assert (=> b!20 (= e!22 (_2!0 (v!71 (unapply!2 (tuple3!1 #x0000002A false Unit!7)))))))
+
+(push 1)
+
+(assert (and (and (and (and (not b!19) (not start!1)) (not b!20)) (not b!18)) (not b!16)))
+
+(check-sat)
+
+(pop 1)
+
+(push 1)
+
+(assert true)
+
+(check-sat)
+
+(pop 1)
+
+(declare-fun d!1 () Bool)
+
+(declare-fun e!25 () Bool)
+
+(assert (=> d!1 e!25))
+
+(declare-fun b!23 () Bool)
+
+(assert (=> (and d!1 (not b!23)) (not e!25)))
+
+(declare-fun Unit!8 () Unit!0)
+
+(declare-fun Unit!9 () Unit!0)
+
+(declare-fun Unit!10 () Unit!0)
+
+(declare-fun Unit!11 () Unit!0)
+
+(assert (=> d!1 (= b!23 (= (unapply!2 (tuple3!1 #x0000002A false Unit!8)) (ite (= (_1!1 (tuple3!1 #x0000002A false Unit!9)) #x00000000) None!1 (Some!1 (tuple2!1 (_3!0 (tuple3!1 #x0000002A false Unit!10)) (_2!1 (tuple3!1 #x0000002A false Unit!11)))))))))
+
+(assert (=> b!23 (= e!25 true)))
+
+(assert (=> b!18 d!1))
+
+(assert (=> start!1 d!1))
+
+(assert (=> b!16 d!1))
+
+(assert (=> b!20 d!1))
+
+(assert (=> b!19 d!1))
+
+(push 1)
+
+(assert true)
+
+(check-sat)
+
+(pop 1)
+
; COMMAND-LINE: --cbqi-all --no-check-models
; EXPECT: sat
+;AJR:BROKEN
(set-logic UFBV)
(set-info :status sat)
(declare-fun Verilog__main.impl_PC_valid_64_1_39_!3 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
cnf-iff-base.smt2 \
cnf-ite.smt2 \
cnf-and-neg.smt2 \
- cnf_abc.smt2
+ cnf_abc.smt2 \
+ bool-pred-nested.smt2
EXTRA_DIST = $(TESTS) \
mkpidgeon
--- /dev/null
+(set-logic QF_UF)
+(set-info :status sat)
+(declare-fun P (Bool Bool) Bool)
+
+(assert (P (P true (P false false)) (P false true)))
+
+(check-sat)
}
void testIffNode() {
- /* Node iffNode(const Node& right) const; */
+ /* Node eqNode(const Node& right) const; */
Node left = d_nodeManager->mkConst(true);
Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
- Node eq = left.iffNode(right);
+ Node eq = left.eqNode(right);
- TS_ASSERT(IFF == eq.getKind());
+ TS_ASSERT(EQUAL == eq.getKind());
TS_ASSERT(2 == eq.getNumChildren());
TS_ASSERT(*(eq.begin()) == left);
Node n = d_nodeManager->mkNode(NOT, a);
TS_ASSERT(NOT == n.getKind());
- n = d_nodeManager->mkNode(IFF, a, b);
- TS_ASSERT(IFF == n.getKind());
+ n = d_nodeManager->mkNode(EQUAL, a, b);
+ TS_ASSERT(EQUAL == n.getKind());
Node x = d_nodeManager->mkSkolem("x", *d_realType);
Node y = d_nodeManager->mkSkolem("y", *d_realType);
d_nodeManager->mkNode(
kind::IMPLIES, d_nodeManager->mkNode(kind::AND, a, b),
d_nodeManager->mkNode(
- kind::IFF, d_nodeManager->mkNode(kind::OR, c, d),
+ kind::EQUAL, d_nodeManager->mkNode(kind::OR, c, d),
d_nodeManager->mkNode(kind::NOT,
d_nodeManager->mkNode(kind::XOR, e, f)))),
false, false, RULE_INVALID, Node::null());
NodeManagerScope nms(d_nodeManager);
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IFF, a, b), false,
+ d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::EQUAL, a, b), false,
false, RULE_INVALID, Node::null());
TS_ASSERT(d_satSolver->addClauseCalled());
}
hfc = d_nm->mkNode(kind::APPLY_UF, h, fc);
gfb = d_nm->mkNode(kind::APPLY_UF, g, fb);
- ac = d_nm->mkNode(kind::IFF, a, c);
- ffbd = d_nm->mkNode(kind::IFF, ffb, d);
- efhc = d_nm->mkNode(kind::IFF, e, fhc);
- dfa = d_nm->mkNode(kind::IFF, d, fa);
+ ac = d_nm->mkNode(kind::EQUAL, a, c);
+ ffbd = d_nm->mkNode(kind::EQUAL, ffb, d);
+ efhc = d_nm->mkNode(kind::EQUAL, e, fhc);
+ dfa = d_nm->mkNode(kind::EQUAL, d, fa);
// this test is designed for >= 10 removal threshold
TS_ASSERT_LESS_THAN_EQUALS(10u,
projects / cvc5.git / commitdiff