From 81fee3a1b81a6a566392a5f0f8fbc654f2e6c08d Mon Sep 17 00:00:00 2001 From: Krystof Hoder Date: Thu, 19 Apr 2012 17:28:38 +0000 Subject: [PATCH] --- Debug/Log_TagDecls.cpp | 12 ++-- Shell/EquivalenceDiscoverer.cpp | 110 ++++++++++++++++++++++++++++---- Shell/EquivalenceDiscoverer.hpp | 5 +- Shell/Options.cpp | 33 ++++++---- Shell/Options.hpp | 19 ++++-- Shell/Preprocess.cpp | 2 +- 6 files changed, 143 insertions(+), 38 deletions(-) diff --git a/Debug/Log_TagDecls.cpp b/Debug/Log_TagDecls.cpp index c4cb5f5bff..c85d953757 100644 --- a/Debug/Log_TagDecls.cpp +++ b/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"), diff --git a/Shell/EquivalenceDiscoverer.cpp b/Shell/EquivalenceDiscoverer.cpp index 9ac5a2e099..05330f6246 100644 --- a/Shell/EquivalenceDiscoverer.cpp +++ b/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,7 +264,11 @@ 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"); @@ -265,7 +276,9 @@ Inference* EquivalenceDiscoverer::getEquivInference(SATLiteral l1, SATLiteral l2 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::Iterator implIt(sswp.getImplications()); + //TODO: make better equivalence retrieval for CR_DEFINITIONS + + if(_discoverImplications) { + const IntUnionFind& eqClasses = sswp.getEquivalenceClasses(); + DHSet::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 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; diff --git a/Shell/EquivalenceDiscoverer.hpp b/Shell/EquivalenceDiscoverer.hpp index 34866daa61..bc1b61b417 100644 --- a/Shell/EquivalenceDiscoverer.hpp +++ b/Shell/EquivalenceDiscoverer.hpp @@ -71,15 +71,16 @@ class EquivalenceDiscoverer { SATSolver& getProofRecordingSolver(); void getImplicationPremises(SATLiteral l1, SATLiteral l2, Stack& 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); diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 394dc979f3..5cb87f49a4 100644 --- a/Shell/Options.cpp +++ b/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; diff --git a/Shell/Options.hpp b/Shell/Options.hpp index 7e0cbe21bd..b479c2a0fe 100644 --- a/Shell/Options.hpp +++ b/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; diff --git a/Shell/Preprocess.cpp b/Shell/Preprocess.cpp index 22efdd97e5..e464536809 100644 --- a/Shell/Preprocess.cpp +++ b/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); }