diff options
Diffstat (limited to 'src/theory/rewriterules/theory_rewriterules.cpp')
| -rw-r--r-- | src/theory/rewriterules/theory_rewriterules.cpp | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index 0d7f5005a..265026b39 100644 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -317,13 +317,14 @@ Answer TheoryRewriteRules::addWatchIfDontKnow(Node g0, const RuleInst* ri, const size_t gid){ /** TODO: Should use the representative of g, but should I keep the mapping for myself? */ - /* If it false in one model (current valuation) it's false for all */ - if (useCurrentModel){ - Node val = getValuation().getValue(g0); - Debug("rewriterules") << "getValue:" << g0 << " = " - << val << " is " << (val == d_false) << std::endl; - if (val == d_false) return AFALSE; - }; + //AJR: removed this code after talking with Francois + ///* If it false in one model (current valuation) it's false for all */ + //if (useCurrentModel){ + // Node val = getValuation().getValue(g0); + // Debug("rewriterules") << "getValue:" << g0 << " = " + // << val << " is " << (val == d_false) << std::endl; + // if (val == d_false) return AFALSE; + //}; /** Currently create a node with a literal */ Node g = getValuation().ensureLiteral(g0); GuardedMap::iterator l_i = d_guardeds.find(g); @@ -508,6 +509,10 @@ Node TheoryRewriteRules::explain(TNode n){ return substGuards(&i, TCache ()); } +void TheoryRewriteRules::collectModelInfo( TheoryModel* m ){ + +} + Theory::PPAssertStatus TheoryRewriteRules::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { addRewriteRule(in); return PP_ASSERT_STATUS_UNSOLVED; |