**/
#include "theory/fp/theory_fp.h"
+#include "theory/theory_model.h"
+
+#include <set>
+#include <stack>
+#include <unordered_set>
+#include <vector>
using namespace std;
namespace removeToFPGeneric {
- Node removeToFPGeneric (TNode node) {
- Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC);
+Node removeToFPGeneric(TNode node) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC);
- FloatingPointToFPGeneric info =
- node.getOperator().getConst<FloatingPointToFPGeneric>();
+ FloatingPointToFPGeneric info =
+ node.getOperator().getConst<FloatingPointToFPGeneric>();
- size_t children = node.getNumChildren();
+ size_t children = node.getNumChildren();
- Node op;
+ Node op;
+ NodeManager *nm = NodeManager::currentNM();
- if (children == 1) {
- op = NodeManager::currentNM()->mkConst(
- FloatingPointToFPIEEEBitVector(info.t.exponent(),
- info.t.significand()));
- return NodeManager::currentNM()->mkNode(op, node[0]);
+ if (children == 1) {
+ op = nm->mkConst(FloatingPointToFPIEEEBitVector(info));
+ return nm->mkNode(op, node[0]);
- } else {
- Assert(children == 2);
- Assert(node[0].getType().isRoundingMode());
-
- TypeNode t = node[1].getType();
-
- if (t.isFloatingPoint()) {
- op = NodeManager::currentNM()->mkConst(
- FloatingPointToFPFloatingPoint(info.t.exponent(),
- info.t.significand()));
- } else if (t.isReal()) {
- op = NodeManager::currentNM()->mkConst(
- FloatingPointToFPReal(info.t.exponent(),
- info.t.significand()));
- } else if (t.isBitVector()) {
- op = NodeManager::currentNM()->mkConst(
- FloatingPointToFPSignedBitVector(info.t.exponent(),
- info.t.significand()));
+ } else {
+ Assert(children == 2);
+ Assert(node[0].getType().isRoundingMode());
- } else {
- throw TypeCheckingExceptionPrivate(
- node,
- "cannot rewrite to_fp generic due to incorrect type of second "
- "argument");
- }
+ TypeNode t = node[1].getType();
- return NodeManager::currentNM()->mkNode(op, node[0], node[1]);
+ if (t.isFloatingPoint()) {
+ op = nm->mkConst(FloatingPointToFPFloatingPoint(info));
+ } else if (t.isReal()) {
+ op = nm->mkConst(FloatingPointToFPReal(info));
+ } else if (t.isBitVector()) {
+ op = nm->mkConst(FloatingPointToFPSignedBitVector(info));
+ } else {
+ throw TypeCheckingExceptionPrivate(
+ node,
+ "cannot rewrite to_fp generic due to incorrect type of second "
+ "argument");
}
- Unreachable("to_fp generic not rewritten");
+ return nm->mkNode(op, node[0], node[1]);
}
+
+ Unreachable("to_fp generic not rewritten");
}
+} // namespace removeToFPGeneric
+
+namespace helper {
+Node buildConjunct(const std::vector<TNode> &assumptions) {
+ if (assumptions.size() == 0) {
+ return NodeManager::currentNM()->mkConst<bool>(true);
+
+ } else if (assumptions.size() == 1) {
+ return assumptions[0];
+ } else {
+ // \todo see bv::utils::flattenAnd
+
+ NodeBuilder<> conjunction(kind::AND);
+ for (std::vector<TNode>::const_iterator it = assumptions.begin();
+ it != assumptions.end(); ++it) {
+ conjunction << *it;
+ }
+
+ return conjunction;
+ }
+}
+} // namespace helper
/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-TheoryFp::TheoryFp(context::Context* c, context::UserContext* u,
- OutputChannel& out, Valuation valuation,
- const LogicInfo& logicInfo)
- : Theory(THEORY_FP, c, u, out, valuation, logicInfo)
-{}/* TheoryFp::TheoryFp() */
+TheoryFp::TheoryFp(context::Context *c, context::UserContext *u,
+ OutputChannel &out, Valuation valuation,
+ const LogicInfo &logicInfo)
+ : Theory(THEORY_FP, c, u, out, valuation, logicInfo),
+ d_notification(*this),
+ d_equalityEngine(d_notification, c, "theory::fp::TheoryFp", true),
+ d_registeredTerms(u),
+ d_conv(u),
+ d_expansionRequested(false),
+ d_conflict(c, false),
+ d_conflictNode(c, Node::null()),
+ d_minMap(u),
+ d_maxMap(u),
+ d_toUBVMap(u),
+ d_toSBVMap(u),
+ d_toRealMap(u) {
+ // Kinds that are to be handled in the congruence closure
+
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ABS);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_NEG);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_PLUS);
+ // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_SUB); // Removed
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_MULT);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_DIV);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_FMA);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_SQRT);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_REM);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_RTI);
+ // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_MIN); // Removed
+ // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_MAX); // Removed
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_MIN_TOTAL);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_MAX_TOTAL);
+
+ // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_EQ); // Removed
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_LEQ);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_LT);
+ // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_GEQ); // Removed
+ // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_GT); // Removed
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISN);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISSN);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISZ);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISINF);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISNAN);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISNEG);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISPOS);
+
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_FP_REAL);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
+ d_equalityEngine.addFunctionKind(
+ kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
+ // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_FP_GENERIC); //
+ // Needed in parsing, should be rewritten away
+ // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_UBV); // Removed
+ // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_SBV); // Removed
+ // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_REAL); // Removed
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_UBV_TOTAL);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_SBV_TOTAL);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_REAL_TOTAL);
-Node TheoryFp::expandDefinition(LogicRequest &, Node node) {
- Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node << std::endl;
+} /* TheoryFp::TheoryFp() */
+
+Node TheoryFp::minUF(Node node) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_MIN);
+ TypeNode t(node.getType());
+ Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ NodeManager *nm = NodeManager::currentNM();
+ ComparisonUFMap::const_iterator i(d_minMap.find(t));
+
+ Node fun;
+ if (i == d_minMap.end()) {
+ std::vector<TypeNode> args(2);
+ args[0] = t;
+ args[1] = t;
+ fun = nm->mkSkolem("floatingpoint_min_zero_case",
+ nm->mkFunctionType(args,
+#ifdef SYMFPUPROPISBOOL
+ nm->booleanType()
+#else
+ nm->mkBitVectorType(1U)
+#endif
+ ),
+ "floatingpoint_min_zero_case",
+ NodeManager::SKOLEM_EXACT_NAME);
+ d_minMap.insert(t, fun);
+ } else {
+ fun = (*i).second;
+ }
+ return nm->mkNode(kind::APPLY_UF, fun, node[1],
+ node[0]); // Application reverses the order or arguments
+}
+
+Node TheoryFp::maxUF(Node node) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_MAX);
+ TypeNode t(node.getType());
+ Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ NodeManager *nm = NodeManager::currentNM();
+ ComparisonUFMap::const_iterator i(d_maxMap.find(t));
+
+ Node fun;
+ if (i == d_maxMap.end()) {
+ std::vector<TypeNode> args(2);
+ args[0] = t;
+ args[1] = t;
+ fun = nm->mkSkolem("floatingpoint_max_zero_case",
+ nm->mkFunctionType(args,
+#ifdef SYMFPUPROPISBOOL
+ nm->booleanType()
+#else
+ nm->mkBitVectorType(1U)
+#endif
+ ),
+ "floatingpoint_max_zero_case",
+ NodeManager::SKOLEM_EXACT_NAME);
+ d_maxMap.insert(t, fun);
+ } else {
+ fun = (*i).second;
+ }
+ return nm->mkNode(kind::APPLY_UF, fun, node[1], node[0]);
+}
+
+Node TheoryFp::toUBVUF(Node node) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV);
+
+ TypeNode target(node.getType());
+ Assert(target.getKind() == kind::BITVECTOR_TYPE);
+
+ TypeNode source(node[1].getType());
+ Assert(source.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ std::pair<TypeNode, TypeNode> p(source, target);
+ NodeManager *nm = NodeManager::currentNM();
+ ConversionUFMap::const_iterator i(d_toUBVMap.find(p));
+
+ Node fun;
+ if (i == d_toUBVMap.end()) {
+ std::vector<TypeNode> args(2);
+ args[0] = nm->roundingModeType();
+ args[1] = source;
+ fun = nm->mkSkolem("floatingpoint_to_ubv_out_of_range_case",
+ nm->mkFunctionType(args, target),
+ "floatingpoint_to_ubv_out_of_range_case",
+ NodeManager::SKOLEM_EXACT_NAME);
+ d_toUBVMap.insert(p, fun);
+ } else {
+ fun = (*i).second;
+ }
+ return nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
+}
+
+Node TheoryFp::toSBVUF(Node node) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV);
+
+ TypeNode target(node.getType());
+ Assert(target.getKind() == kind::BITVECTOR_TYPE);
+
+ TypeNode source(node[1].getType());
+ Assert(source.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ std::pair<TypeNode, TypeNode> p(source, target);
+ NodeManager *nm = NodeManager::currentNM();
+ ConversionUFMap::const_iterator i(d_toSBVMap.find(p));
+
+ Node fun;
+ if (i == d_toSBVMap.end()) {
+ std::vector<TypeNode> args(2);
+ args[0] = nm->roundingModeType();
+ args[1] = source;
+ fun = nm->mkSkolem("floatingpoint_to_sbv_out_of_range_case",
+ nm->mkFunctionType(args, target),
+ "floatingpoint_to_sbv_out_of_range_case",
+ NodeManager::SKOLEM_EXACT_NAME);
+ d_toSBVMap.insert(p, fun);
+ } else {
+ fun = (*i).second;
+ }
+ return nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
+}
+
+Node TheoryFp::toRealUF(Node node) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL);
+ TypeNode t(node[0].getType());
+ Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ NodeManager *nm = NodeManager::currentNM();
+ ComparisonUFMap::const_iterator i(d_toRealMap.find(t));
+
+ Node fun;
+ if (i == d_toRealMap.end()) {
+ std::vector<TypeNode> args(1);
+ args[0] = t;
+ fun = nm->mkSkolem("floatingpoint_to_real_infinity_and_NaN_case",
+ nm->mkFunctionType(t, nm->realType()),
+ "floatingpoint_to_real_infinity_and_NaN_case",
+ NodeManager::SKOLEM_EXACT_NAME);
+ d_toRealMap.insert(t, fun);
+ } else {
+ fun = (*i).second;
+ }
+ return nm->mkNode(kind::APPLY_UF, fun, node[0]);
+}
+
+Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) {
+ Trace("fp-expandDefinition")
+ << "TheoryFp::expandDefinition(): " << node << std::endl;
+
+ if (!this->d_expansionRequested) {
+ lr.widenLogic(
+ THEORY_UF); // Needed for conversions to/from real and min/max
+ lr.widenLogic(THEORY_BV);
+ this->d_expansionRequested = true;
+ }
+
+ Node res = node;
if (node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC) {
- Node res(removeToFPGeneric::removeToFPGeneric(node));
+ res = removeToFPGeneric::removeToFPGeneric(node);
- Trace("fp-expandDefinition") << "TO_FP_GENERIC rewritten to " << res << std::endl;
+ } else if (node.getKind() == kind::FLOATINGPOINT_MIN) {
+ res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MIN_TOTAL,
+ node[0], node[1], minUF(node));
+
+ } else if (node.getKind() == kind::FLOATINGPOINT_MAX) {
+ res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MAX_TOTAL,
+ node[0], node[1], maxUF(node));
+
+ } else if (node.getKind() == kind::FLOATINGPOINT_TO_UBV) {
+ FloatingPointToUBV info = node.getOperator().getConst<FloatingPointToUBV>();
+ FloatingPointToUBVTotal newInfo(info);
+
+ res =
+ NodeManager::currentNM()->mkNode( // kind::FLOATINGPOINT_TO_UBV_TOTAL,
+ NodeManager::currentNM()->mkConst(newInfo), node[0], node[1],
+ toUBVUF(node));
+
+ } else if (node.getKind() == kind::FLOATINGPOINT_TO_SBV) {
+ FloatingPointToSBV info = node.getOperator().getConst<FloatingPointToSBV>();
+ FloatingPointToSBVTotal newInfo(info);
+
+ res =
+ NodeManager::currentNM()->mkNode( // kind::FLOATINGPOINT_TO_SBV_TOTAL,
+ NodeManager::currentNM()->mkConst(newInfo), node[0], node[1],
+ toSBVUF(node));
+
+ } else if (node.getKind() == kind::FLOATINGPOINT_TO_REAL) {
+ res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL,
+ node[0], toRealUF(node));
- return res;
} else {
- return node;
+ // Do nothing
}
+
+ if (res != node) {
+ Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
+ << " rewritten to " << res << std::endl;
+ }
+
+ return res;
}
+void TheoryFp::convertAndEquateTerm(TNode node) {
+ Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl;
+ size_t oldAdditionalAssertions = d_conv.d_additionalAssertions.size();
-void TheoryFp::check(Effort level) {
- if (done() && !fullEffort(level)) {
- return;
+ Node converted(d_conv.convert(node));
+
+ if (converted != node) {
+ Debug("fp-convertTerm")
+ << "TheoryFp::convertTerm(): before " << node << std::endl;
+ Debug("fp-convertTerm")
+ << "TheoryFp::convertTerm(): after " << converted << std::endl;
}
- while(!done()) {
+ size_t newAdditionalAssertions = d_conv.d_additionalAssertions.size();
+ Assert(oldAdditionalAssertions <= newAdditionalAssertions);
+
+ while (oldAdditionalAssertions < newAdditionalAssertions) {
+ Node addA = d_conv.d_additionalAssertions[oldAdditionalAssertions];
+
+ Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion "
+ << addA << std::endl;
+
+#ifdef SYMFPUPROPISBOOL
+ handleLemma(addA, false, true);
+#else
+ NodeManager *nm = NodeManager::currentNM();
+
+ handleLemma(
+ nm->mkNode(kind::EQUAL, addA, nm->mkConst(::CVC4::BitVector(1U, 1U))));
+#endif
+
+ ++oldAdditionalAssertions;
+ }
+
+ // Equate the floating-point atom and the converted one.
+ // Also adds the bit-vectors to the bit-vector solver.
+ if (node.getType().isBoolean()) {
+ if (converted != node) {
+ Assert(converted.getType().isBitVector());
+
+ NodeManager *nm = NodeManager::currentNM();
+
+#ifdef SYMFPUPROPISBOOL
+ handleLemma(nm->mkNode(kind::EQUAL, node, converted));
+#else
+ handleLemma(
+ nm->mkNode(kind::EQUAL, node,
+ nm->mkNode(kind::EQUAL, converted,
+ nm->mkConst(::CVC4::BitVector(1U, 1U)))));
+#endif
+
+ } else {
+ Assert((node.getKind() == kind::EQUAL));
+ }
+
+ } else if (node.getType().isBitVector()) {
+ if (converted != node) {
+ Assert(converted.getType().isBitVector());
+
+ handleLemma(
+ NodeManager::currentNM()->mkNode(kind::EQUAL, node, converted));
+ }
+ }
+
+ return;
+}
+
+void TheoryFp::registerTerm(TNode node) {
+ Trace("fp-registerTerm") << "TheoryFp::registerTerm(): " << node << std::endl;
+
+ if (!isRegistered(node)) {
+ bool success = d_registeredTerms.insert(node);
+ (void)success; // Only used for assertion
+ Assert(success);
+
+ // Add to the equality engine
+ if (node.getKind() == kind::EQUAL) {
+ d_equalityEngine.addTriggerEquality(node);
+ } else {
+ d_equalityEngine.addTerm(node);
+ }
+
+ convertAndEquateTerm(node);
+ }
+ return;
+}
+
+bool TheoryFp::isRegistered(TNode node) {
+ return !(d_registeredTerms.find(node) == d_registeredTerms.end());
+}
+
+void TheoryFp::preRegisterTerm(TNode node) {
+ Trace("fp-preRegisterTerm")
+ << "TheoryFp::preRegisterTerm(): " << node << std::endl;
+ registerTerm(node);
+ return;
+}
+
+void TheoryFp::addSharedTerm(TNode node) {
+ Trace("fp-addSharedTerm")
+ << "TheoryFp::addSharedTerm(): " << node << std::endl;
+ // A system-wide invariant; terms must be registered before they are shared
+ Assert(isRegistered(node));
+ return;
+}
+
+void TheoryFp::handleLemma(Node node) {
+ Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl;
+
+ d_out->lemma(node, false,
+ true); // Has to be true because it contains embedded ITEs
+ // Ignore the LemmaStatus structure for now...
+
+ return;
+}
+
+bool TheoryFp::handlePropagation(TNode node) {
+ Trace("fp") << "TheoryFp::handlePropagation(): propagate " << node
+ << std::endl;
+
+ bool stat = d_out->propagate(node);
+
+ if (!stat) handleConflict(node);
+
+ return stat;
+}
+
+void TheoryFp::handleConflict(TNode node) {
+ Trace("fp") << "TheoryFp::handleConflict(): conflict detected " << node
+ << std::endl;
+
+ d_conflictNode = node;
+ d_conflict = true;
+ d_out->conflict(node);
+ return;
+}
+
+void TheoryFp::check(Effort level) {
+ Trace("fp") << "TheoryFp::check(): started at effort level " << level
+ << std::endl;
+
+ while (!done() && !d_conflict) {
// Get all the assertions
Assertion assertion = get();
TNode fact = assertion.assertion;
Debug("fp") << "TheoryFp::check(): processing " << fact << std::endl;
- // Do the work
- switch(fact.getKind()) {
+ // Only handle equalities; the rest should be handled by
+ // the bit-vector theory
+
+ bool negated = fact.getKind() == kind::NOT;
+ TNode predicate = negated ? fact[0] : fact;
+
+ if (predicate.getKind() == kind::EQUAL) {
+ Assert(!(predicate[0].getType().isFloatingPoint() ||
+ predicate[0].getType().isRoundingMode()) ||
+ isRegistered(predicate[0]));
+ Assert(!(predicate[1].getType().isFloatingPoint() ||
+ predicate[1].getType().isRoundingMode()) ||
+ isRegistered(predicate[1]));
+ registerTerm(predicate); // Needed for float equalities
+
+ if (negated) {
+ Debug("fp-eq") << "TheoryFp::check(): adding dis-equality " << fact[0]
+ << std::endl;
+ d_equalityEngine.assertEquality(predicate, false, fact);
+
+ } else {
+ Debug("fp-eq") << "TheoryFp::check(): adding equality " << fact
+ << std::endl;
+ d_equalityEngine.assertEquality(predicate, true, fact);
+ }
+ } else {
+ // A system-wide invariant; predicates are registered before they are
+ // asserted
+ Assert(isRegistered(predicate));
+
+ if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
+ Debug("fp-eq") << "TheoryFp::check(): adding predicate " << predicate
+ << " is " << !negated << std::endl;
+ d_equalityEngine.assertPredicate(predicate, !negated, fact);
+ }
+ }
+ }
+
+ Trace("fp") << "TheoryFp::check(): completed" << std::endl;
+
+ /* Checking should be handled by the bit-vector engine */
+ return;
+
+} /* TheoryFp::check() */
+
+void TheoryFp::setMasterEqualityEngine(eq::EqualityEngine *eq) {
+ d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
+Node TheoryFp::explain(TNode n) {
+ Trace("fp") << "TheoryFp::explain(): explain " << n << std::endl;
+
+ // All things we assert directly (and not via bit-vector) should
+ // come from the equality engine so this should be sufficient...
+ std::vector<TNode> assumptions;
+
+ bool polarity = n.getKind() != kind::NOT;
+ TNode atom = polarity ? n : n[0];
+ if (atom.getKind() == kind::EQUAL) {
+ d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+ } else {
+ d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+ }
+
+ return helper::buildConjunct(assumptions);
+}
+
+Node TheoryFp::getModelValue(TNode var) {
+ return d_conv.getValue(d_valuation, var);
+}
+
+void TheoryFp::collectModelInfo(TheoryModel *m) {
+ std::set<Node> relevantTerms;
+
+ Trace("fp-collectModelInfo")
+ << "TheoryFp::collectModelInfo(): begin" << std::endl;
+
+ // Work out which variables are needed
+ computeRelevantTerms(relevantTerms);
+
+ if (Trace.isOn("fp-collectModelInfo")) {
+ for (std::set<Node>::const_iterator i(relevantTerms.begin());
+ i != relevantTerms.end(); ++i) {
+ Trace("fp-collectModelInfo")
+ << "TheoryFp::collectModelInfo(): relevantTerms " << *i << std::endl;
+ }
+ }
+
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::stack<TNode> working;
+ std::set<TNode> relevantVariables;
+ for (std::set<Node>::const_iterator i(relevantTerms.begin());
+ i != relevantTerms.end(); ++i) {
+ working.push(*i);
+ }
- /* cases for all the theory's kinds go here... */
+ while (!working.empty()) {
+ TNode current = working.top();
+ working.pop();
- default:
- Unhandled(fact.getKind());
+ // Ignore things that have already been explored
+ if (visited.find(current) == visited.end()) {
+ visited.insert(current);
+
+ TypeNode t(current.getType());
+
+ if ((t.isRoundingMode() || t.isFloatingPoint()) &&
+ this->isLeaf(current)) {
+ relevantVariables.insert(current);
+ }
+
+ for (size_t i = 0; i < current.getNumChildren(); ++i) {
+ working.push(current[i]);
+ }
}
}
-}/* TheoryFp::check() */
+ for (std::set<TNode>::const_iterator i(relevantVariables.begin());
+ i != relevantVariables.end(); ++i) {
+ TNode node = *i;
+
+ Trace("fp-collectModelInfo")
+ << "TheoryFp::collectModelInfo(): relevantVariable " << node
+ << std::endl;
+
+ m->assertEquality(node, d_conv.getValue(d_valuation, node), true);
+ }
+
+ return;
+}
+
+bool TheoryFp::NotifyClass::eqNotifyTriggerEquality(TNode equality,
+ bool value) {
+ Debug("fp-eq")
+ << "TheoryFp::eqNotifyTriggerEquality(): call back as equality "
+ << equality << " is " << value << std::endl;
+
+ if (value) {
+ return d_theorySolver.handlePropagation(equality);
+ } else {
+ return d_theorySolver.handlePropagation(equality.notNode());
+ }
+}
+
+bool TheoryFp::NotifyClass::eqNotifyTriggerPredicate(TNode predicate,
+ bool value) {
+ Debug("fp-eq")
+ << "TheoryFp::eqNotifyTriggerPredicate(): call back as predicate "
+ << predicate << " is " << value << std::endl;
+
+ if (value) {
+ return d_theorySolver.handlePropagation(predicate);
+ } else {
+ return d_theorySolver.handlePropagation(predicate.notNode());
+ }
+}
+
+bool TheoryFp::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1,
+ TNode t2, bool value) {
+ Debug("fp-eq") << "TheoryFp::eqNotifyTriggerTermEquality(): call back as "
+ << t1 << (value ? " = " : " != ") << t2 << std::endl;
+
+ if (value) {
+ return d_theorySolver.handlePropagation(t1.eqNode(t2));
+ } else {
+ return d_theorySolver.handlePropagation(t1.eqNode(t2).notNode());
+ }
+}
+
+void TheoryFp::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+ Debug("fp-eq") << "TheoryFp::eqNotifyConstantTermMerge(): call back as " << t1
+ << " = " << t2 << std::endl;
+
+ std::vector<TNode> assumptions;
+ d_theorySolver.d_equalityEngine.explainEquality(t1, t2, true, assumptions);
+
+ Node conflict = helper::buildConjunct(assumptions);
+
+ d_theorySolver.handleConflict(conflict);
+}
-}/* CVC4::theory::fp namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace fp
+} // namespace theory
+} // namespace CVC4
projects / cvc5.git / commitdiff