No commit message

ModelWriter · Apr 20, 2012 · 76d6f37 · 76d6f37
1 parent 06298e2
commit 76d6f37
Show file tree

Hide file tree

Showing 21 changed files with 526 additions and 359 deletions.
diff --git a/Api/Problem.cpp b/Api/Problem.cpp
@@ -23,6 +23,7 @@
 #include "Kernel/Unit.hpp"
 
 #include "Shell/AIGCompressor.hpp"
+#include "Shell/AIGDefinitionIntroducer.hpp"
 #include "Shell/AIGInliner.hpp"
 #include "Shell/CNF.hpp"
 #include "Shell/EPRInlining.hpp"
@@ -1075,7 +1076,9 @@ class Problem::PredicateEquivalenceDiscoverer
       Kernel::UnitList::push(f.unit, units);
     }
 
-    EquivalenceDiscoverer ed(true, _satConflictCountLimit, _predEquivsOnly);
+    EquivalenceDiscoverer::CandidateRestriction restr =
+	_predEquivsOnly ? EquivalenceDiscoverer::CR_EQUIVALENCES : EquivalenceDiscoverer::CR_NONE;
+    EquivalenceDiscoverer ed(true, _satConflictCountLimit, restr, false);
     if(_restricted) {
       ed.setRestrictedRange(pvi( Stack<Kernel::Literal*>::Iterator(_restrSet1) ),
 	  pvi( Stack<Kernel::Literal*>::Iterator(_restrSet2)) );

diff --git a/Debug/Log_TagDecls.cpp b/Debug/Log_TagDecls.cpp
@@ -589,16 +589,14 @@ void Logging::doTagDeclarations()
       DOC("discovered equivalences"),
       PARENT("pp_ed",1),
       UNIT_TAG);
-  DECL("pp_ed_eq_prems",
-      DOC("premises of discovered equivalences"),
-      PARENT("pp_ed_eq",1));
+  DECL("pp_ed_tl",
+      DOC("discovered true literals"),
+      PARENT("pp_ed",1),
+      UNIT_TAG);
   DECL("pp_ed_imp",
       DOC("discovered implications"),
       PARENT("pp_ed",1),
       UNIT_TAG);
-  DECL("pp_ed_imp_prems",
-      DOC("premises of discovered implications"),
-      PARENT("pp_ed_imp",1));
 
   DECL("pp_aig",
       DOC("aig sub-formula sharing"),
@@ -879,6 +877,9 @@ void Logging::doTagDeclarations()
   DECL("sat_iss_try_impl",
       DOC("attempts to prove implications"),
       PARENT("sat_iss",1));
+  DECL("sat_iss_rot",
+      DOC("information on finished rotations"),
+      PARENT("sat_iss",1));
   DECL("sat_iss_impl_scan",
       DOC("internal working of lookForImplications function"),
       PARENT("sat_iss",2));

diff --git a/Kernel/Problem.cpp b/Kernel/Problem.cpp
@@ -46,6 +46,7 @@ Problem::Problem(UnitList* units)
  * clauses in the iterator.
  */
 Problem::Problem(ClauseIterator clauses, bool copy)
+: _units(0)
 {
   CALL("Problem::Problem(ClauseIterator,bool)");
 
@@ -59,7 +60,7 @@ Problem::Problem(ClauseIterator clauses, bool copy)
     }
     UnitList::push(cl, units);
   }
-  addUnits(_units);
+  addUnits(units);
 
 }