work on sat model minimizer

vutil tool for generation claims to discover predicate equivalences by consequence_elimination
plugging sat equivalence discovery into the system

Api/Problem.cpp

@@ -26,6 +26,7 @@
 #include "Shell/EPRInlining.hpp"
 #include "Shell/EPRSkolem.hpp"
 #include "Shell/EqualityPropagator.hpp"
+#include "Shell/EquivalenceDiscoverer.hpp"
 #include "Shell/Flattening.hpp"
 #include "Shell/FormulaIteExpander.hpp"
 #include "Shell/LispLexer.hpp"
@@ -119,7 +120,8 @@ Problem::PreprocessingOptions::PreprocessingOptions(
   traceClausification(traceClausification),
   traceUnusedPredicateDefinitionRemoval(traceUnusedPredicateDefinitionRemoval),
   predicateIndexIntroduction(false),
-  flatteningTopLevelConjunctions(false)
+  flatteningTopLevelConjunctions(false),
+  predicateEquivalenceDiscovery(false)
 {
   CALL("Problem::PreprocessingOptions::PreprocessingOptions");
 }
@@ -194,10 +196,17 @@ class Problem::PData
 
   AFList*& forms() { return _forms; }
 
+  /** Problem must be non-empty */
+  ApiHelper getApiHelper() {
+    CALL("Problem::PData::getApiHelper");
+    ASS_G(size(),0);
+    return _forms->head()._aux;
+  }
+
   DefaultHelperCore* getCore() {
     CALL("Problem::PData::getCore");
-    if(!_forms) { return 0; }
-    return *_forms->head()._aux;
+    if(size()==0) { return 0; }
+    return *getApiHelper();
   }
 
 private:
@@ -262,11 +271,18 @@ void Problem::addFormula(AnnotatedFormula f)
 
 size_t Problem::size()
 {
-  CALL("Problem::addFormula");
+  CALL("Problem::size");
 
   return _data->size();
 }
 
+bool Problem::empty()
+{
+  CALL("Problem::empty");
+
+  return size()==0;
+}
+
 
 
 ///////////////////////////////////////
@@ -866,6 +882,44 @@ class Problem::UnusedPredicateDefinitionRemover : public ProblemTransformer
   DHMap<Kernel::Unit*, Kernel::Unit*> replacements;
 };
 
+class Problem::PredicateEquivalenceDiscoverer
+{
+public:
+  Problem transform(Problem p)
+  {
+    if(p.empty()) {
+      return p;
+    }
+
+    Kernel::UnitList* units = 0;
+
+    AnnotatedFormulaIterator fit=p.formulas();
+    while(fit.hasNext()) {
+      AnnotatedFormula f=fit.next();
+      Kernel::UnitList::push(f.unit, units);
+    }
+
+    EquivalenceDiscoverer ed(true, false);
+    Kernel::UnitList* eqs = ed.getEquivalences(units);
+    units->destroy();
+
+    if(!eqs) { return p; }
+
+    while(eqs) {
+      Kernel::Unit* u = Kernel::UnitList::pop(eqs);
+      AnnotatedFormula af(u, p._data->getApiHelper());
+      AnnotatedFormula::assignName(af, "equiv");
+      p.addFormula(af);
+      LOG("api_prb_transf","discovered predicate equivalence: "<<af);
+    }
+
+    return PredicateDefinitionInliner(INL_PREDICATE_EQUIVALENCES_ONLY, false).transform(p);
+  }
+
+};
+
+
+
 class Problem::SineSelector : public ProblemTransformer
 {
 public:
@@ -1066,6 +1120,10 @@ Problem Problem::preprocess(const PreprocessingOptions& options)
     res = PredicateDefinitionMerger(options.tracePredicateDefinitionMerging).transform(res);
   }
 
+  if(options.predicateEquivalenceDiscovery) {
+    res = PredicateEquivalenceDiscoverer().transform(res);
+  }
+
   if(options.eprSkolemization) {
     res = EPRSkolemizer(options.traceEPRSkolemization).transform(res);
   }

Api/Problem.hpp

@@ -229,6 +229,11 @@ class Problem
      */
     bool flatteningTopLevelConjunctions;
 
+    /**
+     * Use SAT solver to attempt to discover predicate equivalences
+     */
+    bool predicateEquivalenceDiscovery;
+
     /**
      * Add asymmetric rewriting rule to be used during preprocessing.
      *
@@ -362,6 +367,11 @@ class Problem
    */
   size_t size();
 
+  /**
+   * Return true if problem contains no formulas
+   */
+  bool empty();
+
   /**
    * Output tff type definitions for non-standard types and for all
    * functions and predicates, whose type contains some non-default sort.
@@ -391,6 +401,7 @@ class Problem
   class TopLevelFlattener;
   class VariableEqualityPropagator;
   class PredicateIndexIntroducer;
+  class PredicateEquivalenceDiscoverer;
   class PredicateDefinitionMerger;
   class PredicateDefinitionInliner;
   class EPRRestoringInliner;

Kernel/Formula.cpp

@@ -678,6 +678,22 @@ bool Formula::getSkip()
   return true;
 }
 
+Formula* Formula::trueFormula()
+{
+  CALL("Formula::trueFormula");
+
+  static Formula* res = new Formula(true);
+  return res;
+}
+
+Formula* Formula::falseFormula()
+{
+  CALL("Formula::falseFormula");
+
+  static Formula* res = new Formula(false);
+  return res;
+}
+
 Formula* Formula::quantify(Formula* f)
 {
   Set<unsigned> vars;

Kernel/Formula.hpp

@@ -94,6 +94,9 @@ class Formula
 
   static Formula* quantify(Formula* f);
 
+  static Formula* trueFormula();
+  static Formula* falseFormula();
+
   // use allocator to (de)allocate objects of this class
   CLASS_NAME("Formula");
   USE_ALLOCATOR(Formula);

Kernel/Problem.cpp

@@ -364,4 +364,27 @@ bool Problem::hasFormulaItes() const
 }
 
 
+///////////////////////
+// utility functions
+//
+
+/**
+ * Put predicate numbers present in the problem into @c acc
+ *
+ * The numbers added to acc are not unique.
+ *
+ */
+void Problem::collectPredicates(Stack<unsigned>& acc) const
+{
+  CALL("Problem::collectPredicates");
+
+  UnitList::Iterator uit(units());
+  while(uit.hasNext()) {
+    Unit* u = uit.next();
+    u->collectPredicates(acc);
+  }
+}
+
+
+
 }

Kernel/Problem.hpp

@@ -146,6 +146,10 @@ class Problem {
   }
 
 
+  //utility functions
+
+  void collectPredicates(Stack<unsigned>& acc) const;
+
 private:
 
   void initValues();

Kernel/Sorts.cpp

@@ -180,6 +180,9 @@ bool BaseType::operator==(const BaseType& o) const
     }
   }
   unsigned len = arity();
+  if(len!=o.arity()) {
+    return false;
+  }
   for(unsigned i=0; i<len; i++) {
     if(arg(i)!=o.arg(i)) {
       return false;

Lib/Stack.hpp

@@ -454,6 +454,7 @@ class Stack
   };
 
   typedef Iterator TopFirstIterator;
+  typedef Iterator DelIterator;
 
   /**
    * An iterator object that for stack @b s first yields element s[0]

Makefile

@@ -203,6 +203,7 @@ VINF_OBJ=Inferences/BackwardDemodulation.o\
 
 VSAT_OBJ=SAT/ClauseDisposer.o\
          SAT/DIMACS.o\
+         SAT/MinimizingSolver.o\
          SAT/Preprocess.o\
          SAT/RestartStrategy.o\
          SAT/SATClause.o\
@@ -328,6 +329,7 @@ VUT_OBJ = $(patsubst %.cpp,%.o,$(wildcard UnitTests/*.cpp))
 
 VUTIL_OBJ = VUtils/AnnotationColoring.o\
             VUtils/EPRRestoringScanner.o\
+            VUtils/FOEquivalenceDiscovery.o\
             VUtils/LocalityRestoring.o\
             VUtils/ProblemColoring.o\
             VUtils/RangeColoring.o\
@@ -499,7 +501,7 @@ VCLAUSIFY_DEP = $(VCLAUSIFY_BASIC) Global.o vclausify.o
 VUTIL_DEP = $(VAMP_BASIC) $(VUTIL_OBJ) Global.o vutil.o
 VSAT_DEP = $(VSAT_BASIC) Global.o vsat.o
 VTEST_DEP = $(VAMP_BASIC) $(API_OBJ) $(VT_OBJ) $(VUT_OBJ) Global.o vtest.o
-LIBVAPI_DEP = $(VD_OBJ) $(API_OBJ) $(OTHER_API_DEP) Global.o
+LIBVAPI_DEP = $(VD_OBJ) $(API_OBJ) $(VCLAUSIFY_BASIC) Global.o
 VAPI_DEP =  $(LIBVAPI_DEP) test_vapi.o
 #UCOMPIT_OBJ = $(VCOMPIT_BASIC) Global.o compit2.o compit2_impl.o
 VGROUND_DEP = $(VAMP_BASIC) Global.o vground.o

SAT/MinimizingSolver.cpp

@@ -0,0 +1,88 @@
+/**
+ * @file MinimizingSolver.cpp
+ * Implements class MinimizingSolver.
+ */
+
+#include "MinimizingSolver.hpp"
+
+namespace SAT
+{
+
+MinimizingSolver::MinimizingSolver(SATSolver* inner)
+ : _inner(inner),
+   _assignmentValid(false)
+{
+  CALL("MinimizingSolver::MinimizingSolver");
+
+  _assignmentValid = false;
+}
+
+void MinimizingSolver::ensureVarCnt(unsigned newVarCnt)
+{
+  CALL("MinimizingSolver::ensureVarCnt");
+
+  _inner->ensureVarCnt(newVarCnt);
+  _asgn.expand(newVarCnt);
+  _watcher.expand(newVarCnt);
+  _assignmentValid = false;
+}
+
+void MinimizingSolver::addClauses(SATClauseIterator cit, bool onlyPropagate)
+{
+  CALL("MinimizingSolver::addClauses");
+
+  static SATClauseStack newClauses;
+  newClauses.reset();
+  newClauses.loadFromIterator(cit);
+  _unprocessed.loadFromIterator(SATClauseStack::BottomFirstIterator(newClauses));
+
+  _inner->addClauses(pvi(SATClauseStack::BottomFirstIterator(newClauses)), onlyPropagate);
+  _assignmentValid = false;
+}
+
+SATSolver::VarAssignment MinimizingSolver::getAssignment(unsigned var)
+{
+  CALL("MinimizingSolver::getAssignment");
+  ASS_EQ(_inner->getStatus(), SATISFIABLE);
+
+  if(!_assignmentValid) {
+    updateAssignment();
+  }
+
+  if(!_assumptions.isEmpty() && _assumptions.find(var)) {
+    return _assumptions.get(var) ? SATSolver::TRUE : SATSolver::FALSE;
+  }
+
+  if(_watcher[var].isEmpty()) {
+    return SATSolver::DONT_CARE;
+  }
+  return _asgn[var] ? SATSolver::TRUE : SATSolver::FALSE;
+}
+
+void MinimizingSolver::updateAssignment()
+{
+  CALL("MinimizingSolver::updateAssignment");
+
+  NOT_IMPLEMENTED;
+}
+
+
+void MinimizingSolver::addAssumption(SATLiteral lit, bool onlyPropagate)
+{
+  CALL("MinimizingSolver::addAssumption");
+
+  _assumptions.insert(lit.var(), lit.polarity());
+  _inner->addAssumption(lit, onlyPropagate);
+  _assignmentValid = false;
+}
+
+void MinimizingSolver::retractAllAssumptions()
+{
+  CALL("MinimizingSolver::retractAllAssumptions");
+
+  _assumptions.reset();
+  _inner->retractAllAssumptions();
+}
+
+
+}