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);
delete d_subtheories[i];
}
delete d_abstractionModule;
- delete d_extt;
}
void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
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);
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 ) {
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
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];
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;
}
//we care about the length of this string
registerTerm( t[0], 1 );
}else{
- //d_extt->registerTerm( t );
+ //getExtTheory()->registerTerm( t );
}
}
}
}
//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;
}
}
//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;
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];
//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;
//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;
}
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;
}
}
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" );
}
}
}else{
Trace("strings-extf-debug") << " redundant." << std::endl;
- d_extt->markReduced( n );
+ getExtTheory()->markReduced( n );
}
}
}
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() );
, 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)
Theory::~Theory() {
smtStatisticsRegistry()->unregisterStat(&d_checkTime);
smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
+
+ delete d_extTheory;
}
TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
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));
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) {
}
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
* 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;
/**
/** 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 */
*/
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
* @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 */
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();
d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine);
}
}
-
+
d_curr_model_builder = d_quantEngine->getModelBuilder();
d_curr_model = d_quantEngine->getModel();
} else {
projects / cvc5.git / commitdiff