summaryrefslogtreecommitdiff
path: root/src/theory/fp/theory_fp.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/fp/theory_fp.cpp')
-rw-r--r--src/theory/fp/theory_fp.cpp149
1 files changed, 59 insertions, 90 deletions
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 0c5a92572..4c59b1c06 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -110,7 +110,6 @@ TheoryFp::TheoryFp(context::Context* c,
d_registeredTerms(u),
d_conv(u),
d_expansionRequested(false),
- d_conflict(c, false),
d_conflictNode(c, Node::null()),
d_minMap(u),
d_maxMap(u),
@@ -908,15 +907,6 @@ void TheoryFp::preRegisterTerm(TNode node)
return;
}
-void TheoryFp::notifySharedTerm(TNode node)
-{
- Trace("fp-addSharedTerm")
- << "TheoryFp::notifySharedTerm(): " << 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;
// Preprocess has to be true because it contains embedded ITEs
@@ -926,83 +916,41 @@ void TheoryFp::handleLemma(Node node) {
return;
}
-bool TheoryFp::handlePropagation(TNode node) {
- Trace("fp") << "TheoryFp::handlePropagation(): propagate " << node
- << std::endl;
+bool TheoryFp::propagateLit(TNode node)
+{
+ Trace("fp") << "TheoryFp::propagateLit(): propagate " << node << std::endl;
bool stat = d_out->propagate(node);
if (!stat)
{
- d_conflict = true;
+ d_state.notifyInConflict();
}
return stat;
}
-void TheoryFp::handleConflict(TNode node) {
- Trace("fp") << "TheoryFp::handleConflict(): conflict detected " << node
- << std::endl;
+void TheoryFp::conflictEqConstantMerge(TNode t1, TNode t2)
+{
+ std::vector<TNode> assumptions;
+ d_equalityEngine->explainEquality(t1, t2, true, assumptions);
+
+ Node conflict = helper::buildConjunct(assumptions);
+ Trace("fp") << "TheoryFp::conflictEqConstantMerge(): conflict detected "
+ << conflict << std::endl;
- d_conflictNode = node;
- d_conflict = true;
- d_out->conflict(node);
+ d_conflictNode = conflict;
+ d_state.notifyInConflict();
+ d_out->conflict(conflict);
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.d_assertion;
-
- Debug("fp") << "TheoryFp::check(): processing " << fact << std::endl;
-
- // 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);
- }
- }
- }
-
+void TheoryFp::postCheck(Effort level)
+{
// Resolve the abstractions for the conversion lemmas
if (level == EFFORT_LAST_CALL)
{
Trace("fp") << "TheoryFp::check(): checking abstractions" << std::endl;
- TheoryModel *m = getValuation().getModel();
+ TheoryModel* m = getValuation().getModel();
bool lemmaAdded = false;
for (abstractionMapType::const_iterator i = abstractionMap.begin();
@@ -1017,11 +965,35 @@ void TheoryFp::check(Effort level) {
}
Trace("fp") << "TheoryFp::check(): completed" << std::endl;
-
/* Checking should be handled by the bit-vector engine */
- return;
+}
-} /* TheoryFp::check() */
+bool TheoryFp::preNotifyFact(
+ TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+ if (atom.getKind() == kind::EQUAL)
+ {
+ Assert(!(atom[0].getType().isFloatingPoint()
+ || atom[0].getType().isRoundingMode())
+ || isRegistered(atom[0]));
+ Assert(!(atom[1].getType().isFloatingPoint()
+ || atom[1].getType().isRoundingMode())
+ || isRegistered(atom[1]));
+ registerTerm(atom); // Needed for float equalities
+ }
+ else
+ {
+ // A system-wide invariant; predicates are registered before they are
+ // asserted
+ Assert(isRegistered(atom));
+
+ if (!d_equalityEngine->isFunctionKind(atom.getKind()))
+ {
+ return true;
+ }
+ }
+ return false;
+}
TrustNode TheoryFp::explain(TNode n)
{
@@ -1047,16 +1019,20 @@ Node TheoryFp::getModelValue(TNode var) {
return d_conv.getValue(d_valuation, var);
}
-bool TheoryFp::collectModelInfo(TheoryModel *m)
+bool TheoryFp::collectModelInfo(TheoryModel* m)
{
std::set<Node> relevantTerms;
-
- Trace("fp-collectModelInfo")
- << "TheoryFp::collectModelInfo(): begin" << std::endl;
-
// Work out which variables are needed
computeRelevantTerms(relevantTerms);
+ // this override behavior to not assert equality engine
+ return collectModelValues(m, relevantTerms);
+}
+bool TheoryFp::collectModelValues(TheoryModel* m,
+ const std::set<Node>& relevantTerms)
+{
+ Trace("fp-collectModelInfo")
+ << "TheoryFp::collectModelInfo(): begin" << std::endl;
if (Trace.isOn("fp-collectModelInfo")) {
for (std::set<Node>::const_iterator i(relevantTerms.begin());
i != relevantTerms.end(); ++i) {
@@ -1153,9 +1129,9 @@ bool TheoryFp::NotifyClass::eqNotifyTriggerPredicate(TNode predicate,
<< predicate << " is " << value << std::endl;
if (value) {
- return d_theorySolver.handlePropagation(predicate);
+ return d_theorySolver.propagateLit(predicate);
}
- return d_theorySolver.handlePropagation(predicate.notNode());
+ return d_theorySolver.propagateLit(predicate.notNode());
}
bool TheoryFp::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1,
@@ -1164,22 +1140,15 @@ bool TheoryFp::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1,
<< t1 << (value ? " = " : " != ") << t2 << std::endl;
if (value) {
- return d_theorySolver.handlePropagation(t1.eqNode(t2));
- } else {
- return d_theorySolver.handlePropagation(t1.eqNode(t2).notNode());
+ return d_theorySolver.propagateLit(t1.eqNode(t2));
}
+ return d_theorySolver.propagateLit(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);
+ d_theorySolver.conflictEqConstantMerge(t1, t2);
}
} // namespace fp
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback