Merge branch 'master' into new_interpolation

ModelWriter · Oct 17, 2017 · f286eee · f286eee
2 parents aa3ba19 + 1f28823
commit f286eee
Show file tree

Hide file tree

Showing 187 changed files with 13,019 additions and 15,424 deletions.
diff --git a/Api/Problem.cpp b/Api/Problem.cpp
@@ -329,7 +329,7 @@ class Problem::PData
   }
   ~PData()
   {
-    _forms->destroy();
+    AFList::destroy(_forms);
   }
 
   void incRef() { _refCnt++; }
@@ -347,7 +347,7 @@ class Problem::PData
     CALL("Problem::PData::cloneInto");
     ASS_EQ(obj->_forms, 0);
 
-    obj->_forms=_forms->copy();
+    obj->_forms = AFList::copy(_forms);
   }
 
   void addFormula(AnnotatedFormula f)
@@ -696,7 +696,7 @@ class Problem::AIGInliner : public ProblemTransformer
       Kernel::UnitList::push(f.unit, units);
     }
     _aii.scan(units);
-    units->destroy();
+    Kernel::UnitList::destroy(units);
 
     fit=p.formulas();
     while(fit.hasNext()) {
@@ -741,7 +741,7 @@ class Problem::AIGDefinitionIntroducer : public ProblemTransformer
       Kernel::UnitList::push(f.unit, units);
     }
     _adi.scan(units);
-    units->destroy();
+    Kernel::UnitList::units->destroy(units);
 
     fit=p.formulas();
     while(fit.hasNext()) {
@@ -828,7 +828,7 @@ class Problem::PredicateIndexIntroducer : public ProblemTransformer
       Kernel::UnitList::push(f.unit, units);
     }
     _pii.scan(units);
-    units->destroy();
+    Kernel::UnitList::destroy(units);
 
     fit=p.formulas();
     while(fit.hasNext()) {
@@ -902,7 +902,7 @@ class Problem::PredicateDefinitionMerger : public ProblemTransformer
       Kernel::UnitList::push(f.unit, units);
     }
     _merger.scan(units);
-    units->destroy();
+    Kernel::UnitList::destroy(units);
 
     fit=p.formulas();
     while(fit.hasNext()) {
@@ -1072,7 +1072,7 @@ class Problem::EPRRestoringInliner : public ProblemTransformer
       Kernel::UnitList::push(f.unit, units);
     }
     _eprInliner.scan(units);
-    units->destroy();
+    Kernel::UnitList::destroy(units);
 
     fit=p.formulas();
     while(fit.hasNext()) {
@@ -1134,7 +1134,7 @@ class Problem::EPRSkolemizer : public ProblemTransformer
       Kernel::UnitList::push(f.unit, units);
     }
     _eprSkolem.scan(units);
-    units->destroy();
+    Kernel::UnitList::destroy(units);
 
     fit=p.formulas();
     while(fit.hasNext()) {
@@ -1184,7 +1184,7 @@ class Problem::UnusedPredicateDefinitionRemover : public ProblemTransformer
       Kernel::UnitList::push(f.unit, units);
     }
     pd.collectReplacements(units, replacements);
-    units->destroy();
+        Kernel::UnitList::destroy(units);
 
     fit=p.formulas();
     while(fit.hasNext()) {
@@ -1280,7 +1280,7 @@ class Problem::PredicateEquivalenceDiscoverer
       }
       eqs = ed.getEquivalences(units);
     }
-    units->destroy();
+        Kernel::UnitList::destroy(units);
 
     if(!eqs) { return p; }
 

diff --git a/CASC/CASCMode.cpp b/CASC/CASCMode.cpp
diff --git a/CASC/CASCMode.hpp b/CASC/CASCMode.hpp