No commit message

Debug/Log_TagDecls.cpp

@@ -587,14 +587,18 @@ void Logging::doTagDeclarations()
       PARENT("pp_ed",0));
   DECL("pp_ed_eq",
       DOC("discovered equivalences"),
-      PARENT("pp_ed",0),
+      PARENT("pp_ed",1),
       UNIT_TAG);
   DECL("pp_ed_eq_prems",
       DOC("premises of discovered equivalences"),
       PARENT("pp_ed_eq",1));
-  DECL("pp_ed_asm",
-      DOC("assumptions being asserted into the solver"),
-      PARENT("pp_ed",1));
+  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"),

Shell/EquivalenceDiscoverer.cpp

@@ -104,9 +104,16 @@ bool EquivalenceDiscoverer::isEligible(Literal* l)
   return true;
 }
 
-bool EquivalenceDiscoverer::isEligibleEquiv(Literal* l1, Literal* l2)
+/**
+ * Return true if equivalence or implication between l1 and l2 can be
+ * added to the problem.
+ *
+ * Literals l1 and l2 on its own must already be eligible for processing
+ * (isEligible gives true).
+ */
+bool EquivalenceDiscoverer::isEligiblePair(Literal* l1, Literal* l2)
 {
-  CALL("EquivalenceDiscoverer::isEligibleEquiv");
+  CALL("EquivalenceDiscoverer::isEligiblePair");
   ASS(isEligible(l1));
   ASS(isEligible(l2));
 
@@ -257,15 +264,21 @@ void EquivalenceDiscoverer::getImplicationPremises(SATLiteral l1, SATLiteral l2,
   ps.retractAllAssumptions();
 }
 
-Inference* EquivalenceDiscoverer::getEquivInference(SATLiteral l1, SATLiteral l2)
+/**
+ * If @c implication is true, return inference for implication l1 -> l2,
+ * otherwise return inference for equivalence l1 <-> l2.
+ */
+Inference* EquivalenceDiscoverer::getInference(SATLiteral l1, SATLiteral l2, bool implication)
 {
   CALL("EquivalenceDiscoverer::getEquivInference");
 
   static Stack<UnitSpec> premises;
   ASS(premises.isEmpty());
 
   getImplicationPremises(l1, l2, premises);
-  getImplicationPremises(l2, l1, premises);
+  if(!implication) {
+    getImplicationPremises(l2, l1, premises);
+  }
 
   UnitList* premLst = 0;
 
@@ -290,9 +303,22 @@ void EquivalenceDiscoverer::doISSatDiscovery(UnitList*& res)
     ISSatSweeping::Equiv eq = eqIt.next();
     handleEquivalence(eq.first, eq.second, res);
   }
-
-  const IntUnionFind& eqClasses = sswp.getEquivalenceClasses();
-  DHSet<ISSatSweeping::Impl>::Iterator implIt(sswp.getImplications());
+  //TODO: make better equivalence retrieval for CR_DEFINITIONS
+
+  if(_discoverImplications) {
+    const IntUnionFind& eqClasses = sswp.getEquivalenceClasses();
+    DHSet<ISSatSweeping::Impl>::Iterator implIt(sswp.getImplications());
+    while(implIt.hasNext()) {
+      ISSatSweeping::Impl impl = implIt.next();
+      unsigned v1 = impl.first.var();
+      unsigned v2 = impl.second.var();
+      if(eqClasses.root(v1)==eqClasses.root(v2)) {
+	//this implication is subsumed by some equivalence
+	continue;
+      }
+      handleImplication(impl.first, impl.second, res);
+    }
+  }
 }
 
 Literal* EquivalenceDiscoverer::getFOLit(SATLiteral slit) const
@@ -310,7 +336,6 @@ Literal* EquivalenceDiscoverer::getFOLit(SATLiteral slit) const
 bool EquivalenceDiscoverer::handleEquivalence(SATLiteral l1, SATLiteral l2, UnitList*& eqAcc)
 {
   CALL("EquivalenceDiscoverer::handleEquivalence");
-
   ASS_NEQ(l1.var(), l2.var());
 
   Literal* fl1 = getFOLit(l1);
@@ -322,7 +347,7 @@ bool EquivalenceDiscoverer::handleEquivalence(SATLiteral l1, SATLiteral l2, Unit
     return false;
   }
 
-  if(!isEligibleEquiv(fl1, fl2)) {
+  if(!isEligiblePair(fl1, fl2)) {
     return false;
   }
 
@@ -332,7 +357,7 @@ bool EquivalenceDiscoverer::handleEquivalence(SATLiteral l1, SATLiteral l2, Unit
     eqForm = new QuantifiedFormula(FORALL, freeVars, eqForm);
   }
 
-  Inference* inf = getEquivInference(l1, l2);
+  Inference* inf = getInference(l1, l2, false);
   FormulaUnit* fu = new FormulaUnit(eqForm, inf, Unit::AXIOM);
   UnitList::push(fu, eqAcc);
 
@@ -348,13 +373,56 @@ bool EquivalenceDiscoverer::handleEquivalence(SATLiteral l1, SATLiteral l2, Unit
   return true;
 }
 
+/**
+ * If possible and eligible, add FO version of implication lhs -> rhs into @c eqAcc.
+ */
+bool EquivalenceDiscoverer::handleImplication(SATLiteral lhs, SATLiteral rhs, UnitList*& eqAcc)
+{
+  CALL("EquivalenceDiscoverer::handleImplication");
+  ASS_NEQ(lhs.var(), rhs.var());
+
+  Literal* flhs = getFOLit(lhs);
+  Literal* frhs = getFOLit(rhs);
+
+  static DHMap<unsigned,unsigned> varSorts;
+  varSorts.reset();
+  if(!SortHelper::areSortsValid(flhs, varSorts) || !SortHelper::areSortsValid(frhs, varSorts)) {
+    return false;
+  }
+
+  if(!isEligiblePair(flhs, frhs)) {
+    return false;
+  }
+
+  Formula* eqForm = new BinaryFormula(IMP, new AtomicFormula(flhs), new AtomicFormula(frhs));
+  Formula::VarList* freeVars = eqForm->freeVariables();
+  if(freeVars) {
+    eqForm = new QuantifiedFormula(FORALL, freeVars, eqForm);
+  }
+
+  Inference* inf = getInference(lhs, rhs, true);
+  FormulaUnit* fu = new FormulaUnit(eqForm, inf, Unit::AXIOM);
+  UnitList::push(fu, eqAcc);
+
+  LOG_UNIT("pp_ed_imp",fu);
+  TRACE("pp_ed_imp_prems",
+	UnitSpecIterator uit = InferenceStore::instance()->getParents(UnitSpec(fu));
+	while(uit.hasNext()) {
+	  UnitSpec p = uit.next();
+	  TRACE_OUTPUT_UNIT(p.unit());
+	}
+  );
+
+  return true;
+}
+
 UnitList* EquivalenceDiscoverer::getEquivalences(UnitList* units, const Options* opts)
 {
   CALL("EquivalenceDiscoverer::getEquivalences");
 
   Options prepOpts;
   if(opts) { prepOpts = *opts; }
-  prepOpts.setPredicateEquivalenceDiscovery(false);
+  prepOpts.setPredicateEquivalenceDiscovery(Options::PED_OFF);
 
   Problem prb(units->copy());
 
@@ -390,10 +458,24 @@ bool EquivalenceDiscoveringTransformer::apply(UnitList*& units)
 {
   CALL("EquivalenceDiscoveringTransformer::apply(UnitList*&)");
 
-  EquivalenceDiscoverer::CandidateRestriction restr =
-      _opts.predicateEquivalenceDiscoveryAllAtoms() ? EquivalenceDiscoverer::CR_NONE : EquivalenceDiscoverer::CR_EQUIVALENCES;
+  EquivalenceDiscoverer::CandidateRestriction restr;
+  switch(_opts.predicateEquivalenceDiscovery()) {
+  case Options::PED_ALL_ATOMS:
+    restr = EquivalenceDiscoverer::CR_NONE;
+    break;
+  case Options::PED_DEFINITIONS:
+    restr = EquivalenceDiscoverer::CR_DEFINITIONS;
+    break;
+  case Options::PED_ON:
+    restr = EquivalenceDiscoverer::CR_EQUIVALENCES;
+    break;
+  case Options::PED_OFF:
+  default:
+    ASSERTION_VIOLATION;
+  }
 
-  EquivalenceDiscoverer eqd(true, _opts.predicateEquivalenceDiscoverySatConflictLimit(), restr, false);
+  EquivalenceDiscoverer eqd(true, _opts.predicateEquivalenceDiscoverySatConflictLimit(), restr,
+      _opts.predicateEquivalenceDiscoveryAddImplications());
   UnitList* equivs = eqd.getEquivalences(units, &_opts);
   if(!equivs) {
     return false;

Shell/EquivalenceDiscoverer.hpp

@@ -71,15 +71,16 @@ class EquivalenceDiscoverer {
 
   SATSolver& getProofRecordingSolver();
   void getImplicationPremises(SATLiteral l1, SATLiteral l2, Stack<UnitSpec>& acc);
-  Inference* getEquivInference(SATLiteral l1, SATLiteral l2);
+  Inference* getInference(SATLiteral l1, SATLiteral l2, bool implication);
 
   void addGrounding(Clause* cl);
   void collectRelevantLits();
 
   bool isEligible(Literal* l);
-  bool isEligibleEquiv(Literal* l1, Literal* l2);
+  bool isEligiblePair(Literal* l1, Literal* l2);
 
   bool handleEquivalence(SATLiteral l1, SATLiteral l2, UnitList*& eqAcc);
+  bool handleImplication(SATLiteral lhs, SATLiteral rhs, UnitList*& eqAcc);
 
   void doISSatDiscovery(UnitList*& res);
 

Shell/Options.cpp

@@ -66,6 +66,7 @@ class Options::Constants {
   static const char* _sSplittingComponentSweepingValues[];
   static const char* _sSplittingAddComplementaryValues[];
   static const char* _sSplittingNonsplittableComponentsValues[];
+  static const char* _predicateEquivalenceDiscoveryModeValues[];
 
   static int shortNameIndexes[];
 
@@ -98,6 +99,7 @@ class Options::Constants {
   static NameArray sSplittingComponentSweepingValues;
   static NameArray sSplittingAddComplementaryValues;
   static NameArray sSplittingNonsplittableComponentsValues;
+  static NameArray predicateEquivalenceDiscoveryModeValues;
 }; // class Options::Constants
 
 
@@ -187,7 +189,7 @@ const char* Options::Constants::_optionNames[] = {
   "predicate_definition_inlining",
   "predicate_definition_merging",
   "predicate_equivalence_discovery",
-  "predicate_equivalence_discovery_all_atoms",
+  "predicate_equivalence_discovery_add_implications",
   "predicate_equivalence_discovery_sat_conflict_limit",
   "predicate_index_introduction",
   "problem_name",
@@ -647,6 +649,14 @@ const char* Options::Constants::_sSplittingNonsplittableComponentsValues[] = {
 NameArray Options::Constants::sSplittingNonsplittableComponentsValues(_sSplittingNonsplittableComponentsValues,
 					  sizeof(_sSplittingNonsplittableComponentsValues)/sizeof(char*));
 
+const char* Options::Constants::_predicateEquivalenceDiscoveryModeValues[] = {
+  "all_atoms",
+  "definitions",
+  "off",
+  "on"};
+NameArray Options::Constants::predicateEquivalenceDiscoveryModeValues(_predicateEquivalenceDiscoveryModeValues,
+					  sizeof(_predicateEquivalenceDiscoveryModeValues)/sizeof(char*));
+
 
 
 /**
@@ -743,8 +753,8 @@ Options::Options ()
 
   _predicateDefinitionInlining(INL_OFF),
   _predicateDefinitionMerging(false),
-  _predicateEquivalenceDiscovery(false),
-  _predicateEquivalenceDiscoveryAllAtoms(false),
+  _predicateEquivalenceDiscovery(PED_OFF),
+  _predicateEquivalenceDiscoveryAddImplications(false),
   _predicateEquivalenceDiscoverySatConflictLimit(0),
   _predicateIndexIntroduction(false),
   _problemName("unknown"),
@@ -906,8 +916,8 @@ void Options::set(const char* name,const char* value, int index)
       return;
     case AIG_DEFINITION_INTRODUCTION_THRESHOLD:
       if (Int::stringToUnsignedInt(value,unsignedValue)) {
-	if(unsignedValue<=1) {
-	  USER_ERROR("aig_definition_introduction_threshold must be greater than 1");
+	if(unsignedValue==0) {
+	  USER_ERROR("aig_definition_introduction_threshold must be non-zero");
 	}
 	_aigDefinitionIntroductionThreshold = unsignedValue;
 	return;
@@ -1181,10 +1191,11 @@ void Options::set(const char* name,const char* value, int index)
       _predicateDefinitionMerging = onOffToBool(value,name);
       return;
     case PREDICATE_EQUIVALENCE_DISCOVERY:
-      _predicateEquivalenceDiscovery = onOffToBool(value,name);
+      _predicateEquivalenceDiscovery =
+	  (PredicateEquivalenceDiscoveryMode)Constants::predicateEquivalenceDiscoveryModeValues.find(value);
       return;
-    case PREDICATE_EQUIVALENCE_DISCOVERY_ALL_ATOMS:
-      _predicateEquivalenceDiscoveryAllAtoms = onOffToBool(value,name);
+    case PREDICATE_EQUIVALENCE_DISCOVERY_ADD_IMPLICATIONS:
+      _predicateEquivalenceDiscoveryAddImplications = onOffToBool(value,name);
       return;
     case PREDICATE_EQUIVALENCE_DISCOVERY_SAT_CONFLICT_LIMIT:
       if (Int::stringToUnsignedInt(value,unsignedValue)) {
@@ -2010,10 +2021,10 @@ void Options::outputValue (ostream& str,int optionTag) const
     str << boolToOnOff(_predicateDefinitionMerging);
     return;
   case PREDICATE_EQUIVALENCE_DISCOVERY:
-    str << boolToOnOff(_predicateEquivalenceDiscovery);
+    str << Constants::predicateEquivalenceDiscoveryModeValues[_predicateEquivalenceDiscovery];
     return;
-  case PREDICATE_EQUIVALENCE_DISCOVERY_ALL_ATOMS:
-    str << boolToOnOff(_predicateEquivalenceDiscoveryAllAtoms);
+  case PREDICATE_EQUIVALENCE_DISCOVERY_ADD_IMPLICATIONS:
+    str << boolToOnOff(_predicateEquivalenceDiscoveryAddImplications);
     return;
   case PREDICATE_EQUIVALENCE_DISCOVERY_SAT_CONFLICT_LIMIT:
     str << _predicateEquivalenceDiscoverySatConflictLimit;

Shell/Options.hpp

@@ -132,7 +132,7 @@ class Options
     PREDICATE_DEFINITION_MERGING,
     /** Determines whether SAT solver will be used to discover equivalent predicates */
     PREDICATE_EQUIVALENCE_DISCOVERY,
-    PREDICATE_EQUIVALENCE_DISCOVERY_ALL_ATOMS,
+    PREDICATE_EQUIVALENCE_DISCOVERY_ADD_IMPLICATIONS,
     PREDICATE_EQUIVALENCE_DISCOVERY_SAT_CONFLICT_LIMIT,
     PREDICATE_INDEX_INTRODUCTION,
     PROBLEM_NAME,
@@ -433,6 +433,13 @@ class Options
     SOS_ON = 2
   };
 
+  enum PredicateEquivalenceDiscoveryMode {
+    PED_ALL_ATOMS = 0,
+    PED_DEFINITIONS = 1,
+    PED_OFF = 2,
+    PED_ON = 3,
+  };
+
 public:
   Options ();
   void output (ostream&) const;
@@ -468,9 +475,9 @@ class Options
   void setPredicateDefinitionInlining(InliningMode newVal) { _predicateDefinitionInlining = newVal; }
   bool predicateDefinitionMerging() const { return _predicateDefinitionMerging; }
   void setPredicateDefinitionMerging(bool newValue) { _predicateDefinitionMerging = newValue; }
-  bool predicateEquivalenceDiscovery() const { return _predicateEquivalenceDiscovery; }
-  void setPredicateEquivalenceDiscovery(bool newValue) { _predicateEquivalenceDiscovery = newValue; }
-  bool predicateEquivalenceDiscoveryAllAtoms() const { return _predicateEquivalenceDiscoveryAllAtoms; }
+  PredicateEquivalenceDiscoveryMode predicateEquivalenceDiscovery() const { return _predicateEquivalenceDiscovery; }
+  void setPredicateEquivalenceDiscovery(PredicateEquivalenceDiscoveryMode newValue) { _predicateEquivalenceDiscovery = newValue; }
+  bool predicateEquivalenceDiscoveryAddImplications() const { return _predicateEquivalenceDiscoveryAddImplications; }
   unsigned predicateEquivalenceDiscoverySatConflictLimit() const { return _predicateEquivalenceDiscoverySatConflictLimit; }
   bool predicateIndexIntroduction() const { return _predicateIndexIntroduction; }
   void setPredicateIndexIntroduction(bool newValue) { _predicateIndexIntroduction = newValue; }
@@ -780,8 +787,8 @@ class Options
 
   InliningMode _predicateDefinitionInlining;
   bool _predicateDefinitionMerging;
-  bool _predicateEquivalenceDiscovery;
-  bool _predicateEquivalenceDiscoveryAllAtoms;
+  PredicateEquivalenceDiscoveryMode _predicateEquivalenceDiscovery;
+  bool _predicateEquivalenceDiscoveryAddImplications;
   unsigned _predicateEquivalenceDiscoverySatConflictLimit;
   bool _predicateIndexIntroduction;
   string _problemName;

Shell/Preprocess.cpp

@@ -197,7 +197,7 @@ void Preprocess::preprocess (Problem& prb)
     DistinctProcessor().apply(prb);
   }
 
-  if(_options.predicateEquivalenceDiscovery()) {
+  if(_options.predicateEquivalenceDiscovery()!=Options::PED_OFF) {
     EquivalenceDiscoveringTransformer(_options).apply(prb);
   }