diff --git a/Indexing/LiteralSubstitutionTreeWithoutTop.cpp b/Indexing/LiteralSubstitutionTreeWithoutTop.cpp deleted file mode 100644 index 739f28040e..0000000000 --- a/Indexing/LiteralSubstitutionTreeWithoutTop.cpp +++ /dev/null @@ -1,307 +0,0 @@ -/** - * @file LiteralSubstitutionTreeWithoutTop.cpp - * Implements class LiteralSubstitutionTreeWithoutTop. - */ - -#include "Lib/Environment.hpp" -#include "Lib/Metaiterators.hpp" -#include "Lib/TimeCounter.hpp" - -#include "Kernel/Matcher.hpp" -#include "Kernel/Signature.hpp" -#include "Kernel/SortHelper.hpp" -#include "Kernel/Term.hpp" - -#include "LiteralSubstitutionTreeWithoutTop.hpp" - -namespace Indexing -{ - -LiteralSubstitutionTreeWithoutTop::LiteralSubstitutionTreeWithoutTop() -: SubstitutionTree(0), _posRoot(0), _negRoot(0) // We will not be using _nodes, instead we will use _root -{ - _nextVar=1; -} - -void LiteralSubstitutionTreeWithoutTop::insert(Literal* lit, Clause* cls) -{ - CALL("LiteralSubstitutionTreeWithoutTop::insert"); - handleLiteral(lit,cls,true); -} - -void LiteralSubstitutionTreeWithoutTop::remove(Literal* lit, Clause* cls) -{ - CALL("LiteralSubstitutionTreeWithoutTop::remove"); - handleLiteral(lit,cls,false); -} - -void LiteralSubstitutionTreeWithoutTop::handleLiteral(Literal* lit, Clause* cls, bool insert) -{ - CALL("LiteralSubstitutionTreeWithoutTop::handleLiteral"); - - Literal* normLit=Renaming::normalize(lit); - - Node** _root = lit->polarity() ? &_posRoot : &_negRoot; - - BindingMap svBindings; - svBindings.insert(0,TermList(normLit)); - if(insert) { - SubstitutionTree::insert(_root, svBindings, LeafData(cls, lit)); - } else { - SubstitutionTree::remove(_root, svBindings, LeafData(cls, lit)); - } - -} - -SLQueryResultIterator LiteralSubstitutionTreeWithoutTop::getUnifications(Literal* lit, - bool complementary, bool retrieveSubstitutions) -{ - CALL("LiteralSubstitutionTreeWithoutTop::getUnifications"); - return getResultIterator(lit, - complementary, retrieveSubstitutions); -} - -SLQueryResultIterator LiteralSubstitutionTreeWithoutTop::getGeneralizations(Literal* lit, - bool complementary, bool retrieveSubstitutions) -{ - CALL("LiteralSubstitutionTreeWithoutTop::getGeneralizations"); - - SLQueryResultIterator res= -// getResultIterator(lit, - getResultIterator(lit, - complementary, retrieveSubstitutions); -// ASS_EQ(res.hasNext(), getResultIterator(lit, -// complementary, retrieveSubstitutions).hasNext()); - return res; -} - -SLQueryResultIterator LiteralSubstitutionTreeWithoutTop::getInstances(Literal* lit, - bool complementary, bool retrieveSubstitutions) -{ - CALL("LiteralSubstitutionTreeWithoutTop::getInstances"); - -// return getResultIterator(lit, complementary, true); - - if(retrieveSubstitutions) { -#if VDEBUG - NOT_IMPLEMENTED; -#endif - return getResultIterator(lit, complementary, true); - } - - SLQueryResultIterator res= -// getResultIterator(lit, - getResultIterator(lit, - complementary, retrieveSubstitutions); -// ASS_EQ(res.hasNext(), getResultIterator(lit, -// complementary, retrieveSubstitutions).hasNext()); - return res; -} - -struct LiteralSubstitutionTreeWithoutTop::SLQueryResultFunctor -{ - DECL_RETURN_TYPE(SLQueryResult); - OWN_RETURN_TYPE operator() (const QueryResult& qr) { - return SLQueryResult(qr.first.first->literal, qr.first.first->clause, qr.first.second); - } -}; - -struct LiteralSubstitutionTreeWithoutTop::LDToSLQueryResultFn -{ - DECL_RETURN_TYPE(SLQueryResult); - OWN_RETURN_TYPE operator() (const LeafData& ld) { - return SLQueryResult(ld.literal, ld.clause); - } -}; - -#define QRS_QUERY_BANK 0 -#define QRS_RESULT_BANK 1 - -struct LiteralSubstitutionTreeWithoutTop::LDToSLQueryResultWithSubstFn -{ - LDToSLQueryResultWithSubstFn() - { - _subst=RobSubstitutionSP(new RobSubstitution()); - } - DECL_RETURN_TYPE(SLQueryResult); - OWN_RETURN_TYPE operator() (const LeafData& ld) { - return SLQueryResult(ld.literal, ld.clause, - ResultSubstitution::fromSubstitution(_subst.ptr(), - QRS_QUERY_BANK,QRS_RESULT_BANK)); - } -private: - RobSubstitutionSP _subst; -}; - -struct LiteralSubstitutionTreeWithoutTop::UnifyingContext -{ - UnifyingContext(Literal* queryLit) - : _queryLit(queryLit) {} - bool enter(SLQueryResult qr) - { - ASS(qr.substitution); - RobSubstitution* subst=qr.substitution->tryGetRobSubstitution(); - ASS(subst); - - //This code is used only during variant retrieval, so - //literal commutativity doesn't need to concern us, as - //we normalize the query literal, so the argument order - //of commutative literals is always the right one. - ALWAYS(subst->unifyArgs(_queryLit, QRS_QUERY_BANK, qr.literal, QRS_RESULT_BANK)); - - return true; - } - void leave(SLQueryResult qr) - { - RobSubstitution* subst=qr.substitution->tryGetRobSubstitution(); - ASS(subst); - subst->reset(); - } -private: - Literal* _queryLit; -}; - - -struct LiteralSubstitutionTreeWithoutTop::LeafToLDIteratorFn -{ - DECL_RETURN_TYPE(LDIterator); - OWN_RETURN_TYPE operator() (Leaf* l) { - return l->allChildren(); - } -}; - -struct LiteralSubstitutionTreeWithoutTop::PropositionalLDToSLQueryResultWithSubstFn -{ - PropositionalLDToSLQueryResultWithSubstFn() - { - _subst=ResultSubstitutionSP (new DisjunctQueryAndResultVariablesSubstitution()); - } - DECL_RETURN_TYPE(SLQueryResult); - OWN_RETURN_TYPE operator() (const LeafData& ld) { - ASS_EQ(ld.literal->arity(),0); - return SLQueryResult(ld.literal, ld.clause, _subst); - } -private: - ResultSubstitutionSP _subst; -}; - - -SLQueryResultIterator LiteralSubstitutionTreeWithoutTop::getVariants(Literal* lit, - bool complementary, bool retrieveSubstitutions) -{ - CALL("LiteralSubstitutionTreeWithoutTop::getVariants"); - - bool pol = complementary ? !lit->polarity() : lit->polarity(); - Node* _root = pol ? _posRoot : _negRoot; - - if(_root==0) { - return SLQueryResultIterator::getEmpty(); - } - - if(_root->isLeaf()) { - LDIterator ldit=static_cast(_root)->allChildren(); - if(retrieveSubstitutions) { - // a single substitution will be used for all in ldit, but that's OK - return pvi( getMappingIterator(ldit,PropositionalLDToSLQueryResultWithSubstFn()) ); - } else { - return pvi( getMappingIterator(ldit,LDToSLQueryResultFn()) ); - } - } - - Literal* normLit=Renaming::normalize(lit); - - BindingMap svBindings; - svBindings.insert(0,TermList(normLit)); - Leaf* leaf = findLeaf(_root,svBindings); - if(leaf==0) { - return SLQueryResultIterator::getEmpty(); - } - - LDIterator ldit=leaf->allChildren(); - if(retrieveSubstitutions) { - return pvi( getContextualIterator( - getMappingIterator( - ldit, - LDToSLQueryResultWithSubstFn()), - UnifyingContext(lit)) ); - } else { - return pvi( getMappingIterator(ldit,LDToSLQueryResultFn()) ); - } -} - -SLQueryResultIterator LiteralSubstitutionTreeWithoutTop::getAll() -{ - CALL("LiteralSubstitutionTreeWithoutTop::getAll"); - - return pvi( getMappingIterator( - getMapAndFlattenIterator( - vi( new LeafIterator(this) ), - LeafToLDIteratorFn()), - LDToSLQueryResultFn()) ) ; -} - - -struct LiteralSubstitutionTreeWithoutTop::EqualitySortFilter -{ - DECL_RETURN_TYPE(bool); - - EqualitySortFilter(Literal* queryLit) - : _queryEqSort(SortHelper::getEqualityArgumentSort(queryLit)) {} - - bool operator()(const SLQueryResult& res) - { - CALL("LiteralSubstitutionTreeWithoutTop::EqualitySortFilter::operator()"); - ASS(res.literal->isEquality()); - - unsigned resSort = SortHelper::getEqualityArgumentSort(res.literal); - return resSort==_queryEqSort; - } -private: - unsigned _queryEqSort; -}; - -template -SLQueryResultIterator LiteralSubstitutionTreeWithoutTop::getResultIterator(Literal* lit, - bool complementary, bool retrieveSubstitutions) -{ - CALL("LiteralSubstitutionTreeWithoutTop::getResultIterator"); - - bool pol = complementary ? !lit->polarity() : lit->polarity(); - Node* _root = pol ? _posRoot : _negRoot; - - if(_root==0) { - return SLQueryResultIterator::getEmpty(); - } - - if(_root->isLeaf()) { - LDIterator ldit=static_cast(_root)->allChildren(); - if(retrieveSubstitutions) { - // a single substitution will be used for all in ldit, but that's OK - return pvi( getMappingIterator(ldit,PropositionalLDToSLQueryResultWithSubstFn()) ); - } else { - return pvi( getMappingIterator(ldit,LDToSLQueryResultFn()) ); - } - } - bool useC = false; //TODO TODO TODO - - if(lit->commutative()) { - VirtualIterator qrit1=vi( - new Iterator(this, _root, lit, retrieveSubstitutions,false, true, useC) ); - VirtualIterator qrit2=vi( - new Iterator(this, _root, lit, retrieveSubstitutions, true, true, useC) ); - ASS(lit->isEquality()); - return pvi( - getFilteredIterator( - getMappingIterator( - getConcatenatedIterator(qrit1,qrit2), SLQueryResultFunctor()), - EqualitySortFilter(lit)) - ); - } else { - VirtualIterator qrit=VirtualIterator( - new Iterator(this, _root, lit, retrieveSubstitutions,false,true, useC) ); - return pvi( getMappingIterator(qrit, SLQueryResultFunctor()) ); - } -} - - -} diff --git a/Indexing/LiteralSubstitutionTreeWithoutTop.hpp b/Indexing/LiteralSubstitutionTreeWithoutTop.hpp deleted file mode 100644 index 9b0af80fa0..0000000000 --- a/Indexing/LiteralSubstitutionTreeWithoutTop.hpp +++ /dev/null @@ -1,70 +0,0 @@ -/** - * @file LiteralSubstitutionTreeWithoutTop.hpp - * Defines class LiteralSubstitutionTreeWithoutTop. - * - * @author Giles - * TODO refactor to remove duplication with LiteralSubstitutionTree - */ - - -#ifndef __LiteralSubstitutionTreeWithoutTop__ -#define __LiteralSubstitutionTreeWithoutTop__ - -#include "LiteralIndexingStructure.hpp" -#include "SubstitutionTree.hpp" - -namespace Indexing { - -class LiteralSubstitutionTreeWithoutTop -: public LiteralIndexingStructure, SubstitutionTree -{ -public: - CLASS_NAME(LiteralSubstitutionTreeWithoutTop); - USE_ALLOCATOR(LiteralSubstitutionTreeWithoutTop); - - LiteralSubstitutionTreeWithoutTop(); - - void insert(Literal* lit, Clause* cls); - void remove(Literal* lit, Clause* cls); - void handleLiteral(Literal* lit, Clause* cls, bool insert); - - SLQueryResultIterator getAll(); - - SLQueryResultIterator getUnifications(Literal* lit, - bool complementary, bool retrieveSubstitutions); - - SLQueryResultIterator getGeneralizations(Literal* lit, - bool complementary, bool retrieveSubstitutions); - - SLQueryResultIterator getInstances(Literal* lit, - bool complementary, bool retrieveSubstitutions); - - SLQueryResultIterator getVariants(Literal* lit, - bool complementary, bool retrieveSubstitutions); - -#if VDEBUG - virtual void markTagged(){ SubstitutionTree::markTagged();} - vstring toString() {return SubstitutionTree::toString();} -#endif - -private: - struct SLQueryResultFunctor; - struct LDToSLQueryResultFn; - struct LDToSLQueryResultWithSubstFn; - struct UnifyingContext; - struct PropositionalLDToSLQueryResultWithSubstFn; - struct LeafToLDIteratorFn; - - struct EqualitySortFilter; - - template - SLQueryResultIterator getResultIterator(Literal* lit, - bool complementary, bool retrieveSubstitutions); - - Node* _posRoot; - Node* _negRoot; -}; - -}; - -#endif /* __LiteralSubstitutionTreeWithoutTop__ */ diff --git a/InstGen/IGAlgorithm.cpp b/InstGen/IGAlgorithm.cpp index 7dc05f6710..17dcf8df65 100644 --- a/InstGen/IGAlgorithm.cpp +++ b/InstGen/IGAlgorithm.cpp @@ -71,7 +71,7 @@ IGAlgorithm::IGAlgorithm(Problem& prb,const Options& opt) _selector = LiteralSelector::getSelector(*_ordering, opt, opt.instGenSelection()); } - _use_dm = opt.useDM(); + // _use_dm = opt.useDM(); _use_niceness = (opt.satVarSelector() == Options::SatVarSelector::NICENESS); _passive.setAgeWeightRatio(_opt.ageRatio(), _opt.weightRatio()); @@ -326,6 +326,7 @@ bool IGAlgorithm::startGeneratingClause(Clause* orig, ResultSubstitution& subst, genLits.reset(); + /* // We check and update the dismatching constraints associated // with the clause being instantiated DismatchingContraints* dmatch = 0; @@ -333,6 +334,7 @@ bool IGAlgorithm::startGeneratingClause(Clause* orig, ResultSubstitution& subst, TimeCounter tc(TC_DISMATCHING); _dismatchMap.find(orig,dmatch); } + */ unsigned clen = orig->length(); Literal* origLitGnd = 0; @@ -344,6 +346,7 @@ bool IGAlgorithm::startGeneratingClause(Clause* orig, ResultSubstitution& subst, origLitGnd = glit; } + /* { TimeCounter tc(TC_DISMATCHING); // check dismatching constraint here @@ -356,6 +359,7 @@ bool IGAlgorithm::startGeneratingClause(Clause* orig, ResultSubstitution& subst, return false; } } + */ genLits.push(glit); } @@ -384,7 +388,9 @@ void IGAlgorithm::finishGeneratingClause(Clause* orig, ResultSubstitution& subst env.statistics->instGenGeneratedClauses++; bool added = addClause(res); + (void)added; + /* //Update dismatch constraints if(added && _use_dm) { TimeCounter tc(TC_DISMATCHING); @@ -408,6 +414,7 @@ void IGAlgorithm::finishGeneratingClause(Clause* orig, ResultSubstitution& subst #endif dmatch->add(origLit,dm_with); } + */ } /** @@ -772,6 +779,7 @@ void IGAlgorithm::restartFromBeginning() { CALL("IGAlgorithm::restartFromBeginning"); + /* { TimeCounter tc(TC_DISMATCHING); // throw away dismatching constraints @@ -779,6 +787,7 @@ void IGAlgorithm::restartFromBeginning() while(iit.hasNext()){ delete iit.next(); } _dismatchMap.reset(); } + */ _active.reset(); while(!_passive.isEmpty()) { diff --git a/InstGen/IGAlgorithm.hpp b/InstGen/IGAlgorithm.hpp index 13f22ba407..4840b2abb7 100644 --- a/InstGen/IGAlgorithm.hpp +++ b/InstGen/IGAlgorithm.hpp @@ -23,7 +23,6 @@ #include "Indexing/ClauseVariantIndex.hpp" #include "Indexing/IndexManager.hpp" #include "Indexing/LiteralIndex.hpp" -#include "Indexing/LiteralSubstitutionTreeWithoutTop.hpp" #include "Inferences/GlobalSubsumption.hpp" #include "Inferences/InferenceEngine.hpp" @@ -160,11 +159,10 @@ class IGAlgorithm : public MainLoop { DistinctEqualitySimplifier _distinctEqualitySimplifier; bool _use_niceness; + /* bool _use_dm; - /** - * A struct for holding clause's dms, on per literal basis. - */ + // A struct for holding clause's dms, on per literal basis. struct DismatchingContraints { CLASS_NAME(IGAlgorithm::DismatchingContraints); USE_ALLOCATOR(DismatchingContraints); @@ -201,6 +199,7 @@ class IGAlgorithm : public MainLoop { typedef DHMap DismatchMap; DismatchMap _dismatchMap; + */ /** * The internal representation of all the clauses inside IG diff --git a/Makefile b/Makefile index 911d38cf95..0f7d6a9cde 100644 --- a/Makefile +++ b/Makefile @@ -232,7 +232,6 @@ VI_OBJ = Indexing/AcyclicityIndex.o\ Indexing/LiteralIndex.o\ Indexing/LiteralMiniIndex.o\ Indexing/LiteralSubstitutionTree.o\ - Indexing/LiteralSubstitutionTreeWithoutTop.o\ Indexing/ResultSubstitution.o\ Indexing/SubstitutionTree.o\ Indexing/SubstitutionTree_FastGen.o\ diff --git a/Shell/Options.cpp b/Shell/Options.cpp index d748f4b6b2..406d0f7ea9 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -1171,6 +1171,7 @@ void Options::Options::init() _useHashingVariantIndex.setExperimental(); _useHashingVariantIndex.setRandomChoices({"on","off"}); + /* _use_dm = BoolOptionValue("use_dismatching","dm",false); _use_dm.description="Use dismatching constraints."; // Dismatching constraints didn't work and are being discontinued ... @@ -1179,6 +1180,7 @@ void Options::Options::init() //_use_dm.setExperimental(); _use_dm.setRandomChoices({"on","off"}); _use_dm.reliesOn(_saturationAlgorithm.is(equal(SaturationAlgorithm::INST_GEN))); + */ _nicenessOption = ChoiceOptionValue("niceness_option","none",Niceness::NONE,{"average","none","sum","top"}); _nicenessOption.description=""; diff --git a/Shell/Options.hpp b/Shell/Options.hpp index 09f45aa628..8a808666c0 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -1836,7 +1836,7 @@ class Options bool blockedClauseElimination() const { return _blockedClauseElimination.actualValue; } void setUnusedPredicateDefinitionRemoval(bool newVal) { _unusedPredicateDefinitionRemoval.actualValue = newVal; } bool weightIncrement() const { return _weightIncrement.actualValue; } - bool useDM() const { return _use_dm.actualValue; } + // bool useDM() const { return _use_dm.actualValue; } SatSolver satSolver() const { return _satSolver.actualValue; } //void setSatSolver(SatSolver newVal) { _satSolver = newVal; } SaturationAlgorithm saturationAlgorithm() const { return _saturationAlgorithm.actualValue; } @@ -2355,7 +2355,7 @@ class Options BoolOptionValue _unusedPredicateDefinitionRemoval; BoolOptionValue _blockedClauseElimination; UnsignedOptionValue _updatesByOneConstraint; - BoolOptionValue _use_dm; + // BoolOptionValue _use_dm; BoolOptionValue _weightIncrement; IntOptionValue _whileNumber;