From e87c14798b99ccb586751d291b0eeb3208265bd8 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Tue, 25 May 2010 05:30:40 +0000 Subject: Some initial changes to allow for lemmas on demand. To be done: * Add erasable map Clause* to bool to minisat (backtracks with the solver) * Add map from Clause* to Node (clauses that came from a node) * Add reference counting Literal -> Node to CNFManager * If Literal -> Node refcount goes to zero, the clauses of Node can be erased (if eresable) * If clause is erased for each L in clause L -> Node refcount goes down --- src/theory/arith/theory_arith.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/theory/arith/theory_arith.cpp') diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6ca447ea5..bdc32ab21 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -130,8 +130,8 @@ void TheoryArith::registerTerm(TNode tn){ Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left); slackEqLeft.setAttribute(TheoryArithPropagated(), true); - //TODO this has to be wrong no? - d_out->lemma(slackEqLeft); + //TODO this has to be wrong no? YES (dejan) + // d_out->lemma(slackEqLeft); d_tableau.addRow(slackEqLeft); -- cgit v1.2.3