diff options
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 7 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 59 | ||||
| -rw-r--r-- | src/theory/theory.cpp | 21 | ||||
| -rw-r--r-- | src/theory/theory.h | 87 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 4 |
5 files changed, 94 insertions, 84 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 2fc5fd096..ca7c037ef 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -71,9 +71,9 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, d_extf_range_infer(u), d_extf_collapse_infer(u) { - d_extt = new ExtTheory( this ); - d_extt->addFunctionKind( kind::BITVECTOR_TO_NAT ); - d_extt->addFunctionKind( kind::INT_TO_BITVECTOR ); + setupExtTheory(); + getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT); + getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { d_eagerSolver = new EagerBitblastSolver(this); @@ -114,7 +114,6 @@ TheoryBV::~TheoryBV() { delete d_subtheories[i]; } delete d_abstractionModule; - delete d_extt; } void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5f05003c6..bb226e962 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -97,18 +97,18 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, d_cardinality_lits(u), d_curr_cardinality(c, 0) { - d_extt = new ExtTheory( this ); - d_extt->addFunctionKind( kind::STRING_SUBSTR ); - d_extt->addFunctionKind( kind::STRING_STRIDOF ); - d_extt->addFunctionKind( kind::STRING_ITOS ); - d_extt->addFunctionKind( kind::STRING_U16TOS ); - d_extt->addFunctionKind( kind::STRING_U32TOS ); - d_extt->addFunctionKind( kind::STRING_STOI ); - d_extt->addFunctionKind( kind::STRING_STOU16 ); - d_extt->addFunctionKind( kind::STRING_STOU32 ); - d_extt->addFunctionKind( kind::STRING_STRREPL ); - d_extt->addFunctionKind( kind::STRING_STRCTN ); - d_extt->addFunctionKind( kind::STRING_IN_REGEXP ); + setupExtTheory(); + getExtTheory()->addFunctionKind(kind::STRING_SUBSTR); + getExtTheory()->addFunctionKind(kind::STRING_STRIDOF); + getExtTheory()->addFunctionKind(kind::STRING_ITOS); + getExtTheory()->addFunctionKind(kind::STRING_U16TOS); + getExtTheory()->addFunctionKind(kind::STRING_U32TOS); + getExtTheory()->addFunctionKind(kind::STRING_STOI); + getExtTheory()->addFunctionKind(kind::STRING_STOU16); + getExtTheory()->addFunctionKind(kind::STRING_STOU32); + getExtTheory()->addFunctionKind(kind::STRING_STRREPL); + getExtTheory()->addFunctionKind(kind::STRING_STRCTN); + getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP); // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); @@ -142,7 +142,6 @@ TheoryStrings::~TheoryStrings() { for( std::map< Node, EqcInfo* >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){ delete it->second; } - delete d_extt; } Node TheoryStrings::getRepresentative( Node t ) { @@ -644,7 +643,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { if( options::stringExp() ){ //collect extended functions here: some may not be asserted to strings (such as those with return type Int), // but we need to record them so they are treated properly - d_extt->registerTermRec( n ); + getExtTheory()->registerTermRec( n ); } } //concat terms do not contribute to theory combination? TODO: verify @@ -797,10 +796,10 @@ bool TheoryStrings::needsCheckLastEffort() { void TheoryStrings::checkExtfReductions( int effort ) { //standardize this? //std::vector< Node > nred; - //d_extt->doReductions( effort, nred, false ); + //getExtTheory()->doReductions( effort, nred, false ); std::vector< Node > extf; - d_extt->getActive( extf ); + getExtTheory()->getActive( extf ); Trace("strings-process") << "checking " << extf.size() << " active extf" << std::endl; for( unsigned i=0; i<extf.size(); i++ ){ Node n = extf[i]; @@ -809,7 +808,7 @@ void TheoryStrings::checkExtfReductions( int effort ) { int ret = getReduction( effort, n, nr ); Assert( nr.isNull() ); if( ret!=0 ){ - d_extt->markReduced( extf[i] ); + getExtTheory()->markReduced( extf[i] ); if( options::stringOpt1() && hasProcessed() ){ return; } @@ -859,7 +858,7 @@ void TheoryStrings::eqNotifyNewClass(TNode t){ //we care about the length of this string registerTerm( t[0], 1 ); }else{ - //d_extt->registerTerm( t ); + //getExtTheory()->registerTerm( t ); } } @@ -1017,11 +1016,11 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { } } //register the atom here, since it may not create a new equivalence class - //d_extt->registerTerm( atom ); + //getExtTheory()->registerTerm( atom ); } Trace("strings-pending-debug") << " Now collect terms" << std::endl; //collect extended function terms in the atom - d_extt->registerTermRec( atom ); + getExtTheory()->registerTermRec( atom ); Trace("strings-pending-debug") << " Finished collect terms" << std::endl; } @@ -1148,9 +1147,9 @@ void TheoryStrings::checkInit() { } //infer the equality sendInference( exp, n.eqNode( nc ), "I_Norm" ); - }else if( d_extt->hasFunctionKind( n.getKind() ) ){ + }else if( getExtTheory()->hasFunctionKind( n.getKind() ) ){ //mark as congruent : only process if neither has been reduced - d_extt->markCongruent( nc, n ); + getExtTheory()->markCongruent( nc, n ); } //this node is congruent to another one, we can ignore it Trace("strings-process-debug") << " congruent term : " << n << std::endl; @@ -1310,8 +1309,8 @@ void TheoryStrings::checkExtfEval( int effort ) { std::vector< Node > terms; std::vector< Node > sterms; std::vector< std::vector< Node > > exp; - d_extt->getActive( terms ); - d_extt->getSubstitutedTerms( effort, terms, sterms, exp ); + getExtTheory()->getActive( terms ); + getExtTheory()->getSubstitutedTerms( effort, terms, sterms, exp ); for( unsigned i=0; i<terms.size(); i++ ){ Node n = terms[i]; Node sn = sterms[i]; @@ -1335,7 +1334,7 @@ void TheoryStrings::checkExtfEval( int effort ) { //if rewrites to a constant, then do the inference and mark as reduced if( nrc.isConst() ){ if( effort<3 ){ - d_extt->markReduced( n ); + getExtTheory()->markReduced( n ); Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl; std::vector< Node > exps; Trace("strings-extf-debug") << " get symbolic definition..." << std::endl; @@ -1395,7 +1394,7 @@ void TheoryStrings::checkExtfEval( int effort ) { //if it reduces to a conjunction, infer each and reduce }else if( ( nrc.getKind()==kind::OR && itit->second.d_pol==-1 ) || ( nrc.getKind()==kind::AND && itit->second.d_pol==1 ) ){ Assert( effort<3 ); - d_extt->markReduced( n ); + getExtTheory()->markReduced( n ); itit->second.d_exp.push_back( itit->second.d_pol==-1 ? n.negate() : n ); Trace("strings-extf-debug") << " decomposable..." << std::endl; Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << ", pol = " << itit->second.d_pol << std::endl; @@ -1425,7 +1424,7 @@ void TheoryStrings::checkExtfEval( int effort ) { } Trace("strings-extf-list") << std::endl; } - if( d_extt->isActive( n ) && itit->second.d_model_active ){ + if( getExtTheory()->isActive( n ) && itit->second.d_model_active ){ has_nreduce = true; } } @@ -1457,7 +1456,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef children[index] = nr[index][i]; Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, children ); //can mark as reduced, since model for n => model for conc - d_extt->markReduced( conc ); + getExtTheory()->markReduced( conc ); sendInference( in.d_exp, in.d_pol==1 ? conc : conc.negate(), "CTN_Decompose" ); } @@ -1494,7 +1493,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef } }else{ Trace("strings-extf-debug") << " redundant." << std::endl; - d_extt->markReduced( n ); + getExtTheory()->markReduced( n ); } } } @@ -4290,7 +4289,7 @@ bool TheoryStrings::checkMemberships2() { void TheoryStrings::checkMemberships() { //add the memberships std::vector< Node > mems; - d_extt->getActive( mems, kind::STRING_IN_REGEXP ); + getExtTheory()->getActive( mems, kind::STRING_IN_REGEXP ); for( unsigned i=0; i<mems.size(); i++ ){ Node n = mems[i]; Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() ); diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index ab72bf55f..3aa468e01 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -66,7 +66,7 @@ Theory::Theory(TheoryId id, context::Context* satContext, , d_sharedTermsIndex(satContext, 0) , d_careGraph(NULL) , d_quantEngine(NULL) - , d_extt(NULL) + , d_extTheory(NULL) , d_checkTime(getFullInstanceName() + "::checkTime") , d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime") , d_sharedTerms(satContext) @@ -81,6 +81,8 @@ Theory::Theory(TheoryId id, context::Context* satContext, Theory::~Theory() { smtStatisticsRegistry()->unregisterStat(&d_checkTime); smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime); + + delete d_extTheory; } TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { @@ -296,6 +298,11 @@ std::pair<bool, Node> Theory::entailmentCheck( return make_pair(false, Node::null()); } +ExtTheory* Theory::getExtTheory() { + Assert(d_extTheory != NULL); + return d_extTheory; +} + void Theory::addCarePair(TNode t1, TNode t2) { if (d_careGraph) { d_careGraph->insert(CarePair(t1, t2, d_id)); @@ -312,6 +319,18 @@ void Theory::getCareGraph(CareGraph* careGraph) { d_careGraph = NULL; } +void Theory::setQuantifiersEngine(QuantifiersEngine* qe) { + Assert(d_quantEngine == NULL); + Assert(qe != NULL); + d_quantEngine = qe; +} + +void Theory::setupExtTheory() { + Assert(d_extTheory == NULL); + d_extTheory = new ExtTheory(this); +} + + EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid) : d_tid(tid) { } diff --git a/src/theory/theory.h b/src/theory/theory.h index ce94e362e..8f6efcf36 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -85,9 +85,7 @@ private: Theory(const Theory&) CVC4_UNDEFINED; Theory& operator=(const Theory&) CVC4_UNDEFINED; - /** - * An integer identifying the type of the theory - */ + /** An integer identifying the type of the theory. */ TheoryId d_id; /** Name of this theory instance. Along with the TheoryId this should provide @@ -95,19 +93,13 @@ private: * this to ensure unique statistics names over multiple theory instances. */ std::string d_instanceName; - /** - * The SAT search context for the Theory. - */ + /** The SAT search context for the Theory. */ context::Context* d_satContext; - /** - * The user level assertion context for the Theory. - */ + /** The user level assertion context for the Theory. */ context::UserContext* d_userContext; - /** - * Information about the logic we're operating within. - */ + /** Information about the logic we're operating within. */ const LogicInfo& d_logicInfo; /** @@ -121,31 +113,26 @@ private: /** Index into the head of the facts list */ context::CDO<unsigned> d_factsHead; - /** - * Add shared term to the theory. - */ + /** Add shared term to the theory. */ void addSharedTermInternal(TNode node); - /** - * Indices for splitting on the shared terms. - */ + /** Indices for splitting on the shared terms. */ context::CDO<unsigned> d_sharedTermsIndex; - /** - * The care graph the theory will use during combination. - */ + /** The care graph the theory will use during combination. */ CareGraph* d_careGraph; /** - * Reference to the quantifiers engine (or NULL, if quantifiers are - * not supported or not enabled). + * Pointer to the quantifiers engine (or NULL, if quantifiers are not + * supported or not enabled). Not owned by the theory. */ QuantifiersEngine* d_quantEngine; -protected: + /** Extended theory module or NULL. Owned by the theory. */ + ExtTheory* d_extTheory; + + protected: - /** extended theory */ - ExtTheory * d_extt; // === STATISTICS === /** time spent in check calls */ @@ -470,12 +457,11 @@ public: */ virtual void setMasterEqualityEngine(eq::EqualityEngine* eq) { } - /** - * Called to set the quantifiers engine. - */ - virtual void setQuantifiersEngine(QuantifiersEngine* qe) { - d_quantEngine = qe; - } + /** Called to set the quantifiers engine. */ + virtual void setQuantifiersEngine(QuantifiersEngine* qe); + + /** Setup an ExtTheory module for this Theory. Can only be called once. */ + void setupExtTheory(); /** * Return the current theory care graph. Theories should overload @@ -829,31 +815,38 @@ public: * @return a pair <b,E> s.t. if b is true, then a formula E such that * E |= lit in the theory. */ - virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL); + virtual std::pair<bool, Node> entailmentCheck( + TNode lit, const EntailmentCheckParameters* params = NULL, + EntailmentCheckSideEffects* out = NULL); /* equality engine TODO: use? */ - virtual eq::EqualityEngine * getEqualityEngine() { return NULL; } - - /* get extended theory */ - virtual ExtTheory * getExtTheory() { return d_extt; } + virtual eq::EqualityEngine* getEqualityEngine() { return NULL; } + + /* Get extended theory if one has been installed. */ + ExtTheory* getExtTheory(); /* get current substitution at an effort * input : vars - * output : subs, exp + * output : subs, exp * where ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i - */ - virtual bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { return false; } - - /* get reduction for node - if return value is not 0, then n is reduced. - if return value <0 then n is reduced SAT-context-independently (e.g. by a lemma that persists at this user-context level). - if nr is non-null, then ( n = nr ) should be added as a lemma by caller, and return value should be <0. */ - virtual int getReduction( int effort, Node n, Node& nr ) { return 0; } + virtual bool getCurrentSubstitution(int effort, std::vector<Node>& vars, + std::vector<Node>& subs, + std::map<Node, std::vector<Node> >& exp) { + return false; + } /** - * Turn on proof-production mode. + * Get reduction for node + * If return value is not 0, then n is reduced. + * If return value <0 then n is reduced SAT-context-independently (e.g. by a + * lemma that persists at this user-context level). + * If nr is non-null, then ( n = nr ) should be added as a lemma by caller, + * and return value should be <0. */ + virtual int getReduction( int effort, Node n, Node& nr ) { return 0; } + + /** Turn on proof-production mode. */ void produceProofs() { d_proofsEnabled = true; } };/* class Theory */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d297595e1..c7d200a90 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -213,7 +213,7 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf) void TheoryEngine::finishInit() { // initialize the quantifiers engine d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); - + //initialize the quantifiers engine, master equality engine, model, model builder if( d_logicInfo.isQuantified() ) { d_quantEngine->finishInit(); @@ -226,7 +226,7 @@ void TheoryEngine::finishInit() { d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine); } } - + d_curr_model_builder = d_quantEngine->getModelBuilder(); d_curr_model = d_quantEngine->getModel(); } else { |