summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/bv/aig_bitblaster.cpp1
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.cpp17
-rw-r--r--src/theory/bv/bv_subtheory_core.cpp11
-rw-r--r--src/theory/bv/bv_subtheory_core.h5
-rw-r--r--src/theory/bv/bv_subtheory_inequality.cpp16
-rw-r--r--src/theory/bv/eager_bitblaster.cpp2
-rw-r--r--src/theory/bv/kinds1
-rw-r--r--src/theory/bv/lazy_bitblaster.cpp11
-rw-r--r--src/theory/bv/theory_bv.cpp66
-rw-r--r--src/theory/bv/theory_bv.h1
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h8
-rw-r--r--src/theory/bv/theory_bv_rewriter.cpp27
-rw-r--r--src/theory/bv/theory_bv_type_rules.h13
-rw-r--r--src/theory/bv/theory_bv_utils.h6
-rw-r--r--src/theory/strings/theory_strings.cpp16
-rw-r--r--src/theory/strings/theory_strings.h2
-rw-r--r--src/theory/theory.cpp15
-rw-r--r--src/theory/theory.h3
18 files changed, 181 insertions, 40 deletions
diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index 37e9f4476..bb2c403aa 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -276,6 +276,7 @@ void AigBitblaster::bbTerm(TNode node, Bits& bits) {
getBBTerm(node, bits);
return;
}
+ Assert( node.getType().isBitVector() );
Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
d_termBBStrategies[node.getKind()] (node, bits, this);
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 6c6c13ee8..7b7d38307 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -107,6 +107,9 @@ void BitblastSolver::bitblastQueue() {
// don't bit-blast lemma atoms
continue;
}
+ if( !utils::isBitblastAtom(atom) ){
+ continue;
+ }
Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n";
{
TimerStat::CodeTimer codeTimer(d_bitblaster->d_statistics.d_bitblastTimer);
@@ -121,6 +124,7 @@ bool BitblastSolver::check(Theory::Effort e) {
++(d_statistics.d_numCallstoCheck);
+ Debug("bv-bitblast-debug") << "...process queue" << std::endl;
//// Lazy bit-blasting
// bit-blast enqueued nodes
bitblastQueue();
@@ -138,6 +142,10 @@ bool BitblastSolver::check(Theory::Effort e) {
continue;
}
}
+ //skip facts involving integer equalities (from bv2nat)
+ if( !utils::isBitblastAtom( fact ) ){
+ continue;
+ }
if (!d_bv->inConflict() &&
(!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
@@ -154,6 +162,7 @@ bool BitblastSolver::check(Theory::Effort e) {
}
}
+ Debug("bv-bitblast-debug") << "...do propagation" << std::endl;
// We need to ensure we are fully propagated, so propagate now
if (d_useSatPropagation) {
d_bv->spendResource(1);
@@ -167,6 +176,7 @@ bool BitblastSolver::check(Theory::Effort e) {
}
// Solving
+ Debug("bv-bitblast-debug") << "...do solving" << std::endl;
if (e == Theory::EFFORT_FULL) {
Assert(!d_bv->inConflict());
Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n";
@@ -180,6 +190,7 @@ bool BitblastSolver::check(Theory::Effort e) {
}
}
+ Debug("bv-bitblast-debug") << "...do abs bb" << std::endl;
if (options::bvAbstraction() &&
e == Theory::EFFORT_FULL &&
d_lemmaAtomsQueue.size()) {
@@ -187,9 +198,11 @@ bool BitblastSolver::check(Theory::Effort e) {
// bit-blast lemma atoms
while(!d_lemmaAtomsQueue.empty()) {
TNode lemma_atom = d_lemmaAtomsQueue.front();
- d_bitblaster->bbAtom(lemma_atom);
d_lemmaAtomsQueue.pop();
-
+ if( !utils::isBitblastAtom( lemma_atom ) ){
+ continue;
+ }
+ d_bitblaster->bbAtom(lemma_atom);
// Assert to sat and check for conflicts
bool ok = d_bitblaster->assertToSat(lemma_atom, d_useSatPropagation);
if (!ok) {
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 97cbdb215..c59da27f4 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -74,6 +74,8 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
// d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
// d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
// d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
+ d_equalityEngine.addFunctionKind(kind::BITVECTOR_TO_NAT);
+ d_equalityEngine.addFunctionKind(kind::INT_TO_BITVECTOR);
}
CoreSolver::~CoreSolver() {
@@ -368,6 +370,10 @@ void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
d_solver.conflict(t1, t2);
}
+void CoreSolver::NotifyClass::eqNotifyNewClass(TNode t) {
+ d_solver.eqNotifyNewClass( t );
+}
+
bool CoreSolver::storePropagation(TNode literal) {
return d_bv->storePropagation(literal, SUB_CORE);
}
@@ -379,6 +385,11 @@ void CoreSolver::conflict(TNode a, TNode b) {
d_bv->setConflict(conflict);
}
+void CoreSolver::eqNotifyNewClass(TNode t) {
+ Assert( d_bv->getExtTheory()!=NULL );
+ d_bv->getExtTheory()->registerTerm( t );
+}
+
bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
if (d_useSlicer)
return utils::isCoreTerm(term, seen);
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 93a938cc0..22219b5d0 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -53,7 +53,7 @@ class CoreSolver : public SubtheorySolver {
bool eqNotifyTriggerPredicate(TNode predicate, bool value);
bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
void eqNotifyConstantTermMerge(TNode t1, TNode t2);
- void eqNotifyNewClass(TNode t) { }
+ void eqNotifyNewClass(TNode t);
void eqNotifyPreMerge(TNode t1, TNode t2) { }
void eqNotifyPostMerge(TNode t1, TNode t2) { }
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
@@ -72,6 +72,9 @@ class CoreSolver : public SubtheorySolver {
/** Store a conflict from merging two constants */
void conflict(TNode a, TNode b);
+ /** new equivalence class */
+ void eqNotifyNewClass(TNode t);
+
Slicer* d_slicer;
context::CDO<bool> d_isComplete;
unsigned d_lemmaThreshold;
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 7d68f19b2..1fe096214 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -40,14 +40,18 @@ bool InequalitySolver::check(Theory::Effort e) {
Debug("bv-subtheory-inequality") << " "<< fact <<"\n";
if (fact.getKind() == kind::EQUAL) {
TNode a = fact[0];
- TNode b = fact[1];
- ok = addInequality(a, b, false, fact);
- if (ok)
- ok = addInequality(b, a, false, fact);
+ if( a.getType().isBitVector() ){
+ TNode b = fact[1];
+ ok = addInequality(a, b, false, fact);
+ if (ok)
+ ok = addInequality(b, a, false, fact);
+ }
} else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) {
TNode a = fact[0][0];
- TNode b = fact[0][1];
- ok = d_inequalityGraph.addDisequality(a, b, fact);
+ if( a.getType().isBitVector() ){
+ TNode b = fact[0][1];
+ ok = d_inequalityGraph.addDisequality(a, b, fact);
+ }
}
if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) {
TNode a = fact[0][1];
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 53fb4f94b..e66b7f621 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -137,6 +137,8 @@ bool EagerBitblaster::hasBBAtom(TNode atom) const {
}
void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
+ Assert( node.getType().isBitVector() );
+
if (hasBBTerm(node)) {
getBBTerm(node, bits);
return;
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 3cbc45cd1..0ab33379f 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -191,6 +191,7 @@ typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule
+typerule INT_TO_BITVECTOR_OP ::CVC4::theory::bv::IntToBitVectorOpTypeRule
typerule INT_TO_BITVECTOR ::CVC4::theory::bv::BitVectorConversionTypeRule
endtheory
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index b549c329a..fd21456ee 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -94,12 +94,13 @@ void TLazyBitblaster::bbAtom(TNode node) {
if (hasBBAtom(node)) {
return;
}
-
+
// make sure it is marked as an atom
addAtom(node);
Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
++d_statistics.d_numAtoms;
+
/// if we are using bit-vector abstraction bit-blast the original interpretation
if (options::bvAbstraction() &&
@@ -174,7 +175,9 @@ void TLazyBitblaster::makeVariable(TNode var, Bits& bits) {
uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen) {
node = node.getKind() == kind::NOT? node[0] : node;
-
+ if( !utils::isBitblastAtom( node ) ){
+ return 0;
+ }
Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
uint64_t size = utils::numNodes(atom_bb, seen);
return size;
@@ -191,9 +194,10 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
getBBTerm(node, bits);
return;
}
+ Assert( node.getType().isBitVector() );
d_bv->spendResource(options::bitblastStep());
- Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
+ Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
++d_statistics.d_numTerms;
d_termBBStrategies[node.getKind()] (node, bits,this);
@@ -250,6 +254,7 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
} else {
atom = lit;
}
+ Assert( utils::isBitblastAtom( atom ) );
Assert (hasBBAtom(atom));
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index de596e3d5..7bcd23344 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -68,6 +68,9 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
d_isCoreTheory(false),
d_calledPreregister(false)
{
+ d_extt = new ExtTheory( this );
+ d_extt->addFunctionKind( kind::BITVECTOR_TO_NAT );
+ d_extt->addFunctionKind( kind::INT_TO_BITVECTOR );
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
d_eagerSolver = new EagerBitblastSolver(this);
@@ -108,6 +111,7 @@ TheoryBV::~TheoryBV() {
delete d_subtheories[i];
}
delete d_abstractionModule;
+ delete d_extt;
}
void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -324,6 +328,9 @@ void TheoryBV::preRegisterTerm(TNode node) {
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
d_subtheories[i]->preRegister(node);
}
+
+ // AJR : equality solver currently registers all terms, if we want a lazy reduction without the bv equality solver, need to call this
+ //getExtTheory()->registerTermRec( node );
}
void TheoryBV::sendConflict() {
@@ -442,8 +449,22 @@ void TheoryBV::check(Effort e)
}
if (complete) {
// if the last subtheory was complete we stop
+ break;
+ }
+ }
+
+ //check extended functions
+ if (Theory::fullEffort(e)) {
+ //do inferences (adds external lemmas) TODO: this can be improved to add internal inferences
+ std::vector< Node > nred;
+ if( getExtTheory()->doInferences( 0, nred ) ){
+ return;
+ }
+ std::vector< Node > nredr;
+ if( getExtTheory()->doReductions( 0, nred, nredr ) ){
return;
}
+ Assert( nredr.empty() );
}
}
@@ -497,12 +518,12 @@ void TheoryBV::propagate(Effort e) {
}
}
+
eq::EqualityEngine * TheoryBV::getEqualityEngine() {
return NULL;
}
bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
-#if 0
CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
if( core ){
//get the constant equivalence classes
@@ -510,7 +531,7 @@ bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, st
for( unsigned i=0; i<vars.size(); i++ ){
Node n = vars[i];
if( core->getEqualityEngine()->hasTerm( n ) ){
- Node nr = core->getEqualityEngine()->getRepresenative( n );
+ Node nr = core->getEqualityEngine()->getRepresentative( n );
if( nr.isConst() ){
subs.push_back( nr );
exp[n].push_back( n.eqNode( nr ) );
@@ -518,14 +539,53 @@ bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, st
}else{
subs.push_back( n );
}
+ }else{
+ subs.push_back( n );
}
}
//return true if the substitution is non-trivial
return retVal;
}
-#endif
return false;
}
+
+int TheoryBV::getReduction( int effort, Node n, Node& nr ) {
+ Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl;
+ if( n.getKind()==kind::BITVECTOR_TO_NAT ){
+ //taken from rewrite code
+ const unsigned size = utils::getSize(n[0]);
+ NodeManager* const nm = NodeManager::currentNM();
+ const Node z = nm->mkConst(Rational(0));
+ const Node bvone = nm->mkConst(BitVector(1u, 1u));
+ NodeBuilder<> result(kind::PLUS);
+ Integer i = 1;
+ for(unsigned bit = 0; bit < size; ++bit, i *= 2) {
+ Node cond = nm->mkNode(kind::EQUAL, nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), n[0]), bvone);
+ result << nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z);
+ }
+ nr = Node(result);
+ return -1;
+ }else if( n.getKind()==kind::INT_TO_BITVECTOR ){
+ //taken from rewrite code
+ const unsigned size = n.getOperator().getConst<IntToBitVector>().size;
+ NodeManager* const nm = NodeManager::currentNM();
+ const Node bvzero = nm->mkConst(BitVector(1u, 0u));
+ const Node bvone = nm->mkConst(BitVector(1u, 1u));
+ std::vector<Node> v;
+ Integer i = 2;
+ while(v.size() < size) {
+ Node cond = nm->mkNode(kind::GEQ, nm->mkNode(kind::INTS_MODULUS_TOTAL, n[0], nm->mkConst(Rational(i))), nm->mkConst(Rational(i, 2)));
+ cond = Rewriter::rewrite( cond );
+ v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
+ i *= 2;
+ }
+ NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+ result.append(v.rbegin(), v.rend());
+ nr = Node(result);
+ return -1;
+ }
+ return 0;
+}
Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
switch(in.getKind()) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 0709ca427..3cf471356 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -82,6 +82,7 @@ public:
/** equality engine */
eq::EqualityEngine * getEqualityEngine();
bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
+ int getReduction( int effort, Node n, Node& nr );
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 2bcb6ca1b..052bc8c1a 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -239,6 +239,10 @@ template<>
Node RewriteRule<BVToNatEliminate>::apply(TNode node) {
Debug("bv-rewrite") << "RewriteRule<BVToNatEliminate>(" << node << ")" << std::endl;
+ //if( node[0].isConst() ){
+ //TODO? direct computation instead of term construction+rewriting
+ //}
+
const unsigned size = utils::getSize(node[0]);
NodeManager* const nm = NodeManager::currentNM();
const Node z = nm->mkConst(Rational(0));
@@ -263,6 +267,10 @@ template<>
Node RewriteRule<IntToBVEliminate>::apply(TNode node) {
Debug("bv-rewrite") << "RewriteRule<IntToBVEliminate>(" << node << ")" << std::endl;
+ //if( node[0].isConst() ){
+ //TODO? direct computation instead of term construction+rewriting
+ //}
+
const unsigned size = node.getOperator().getConst<IntToBitVector>().size;
NodeManager* const nm = NodeManager::currentNM();
const Node bvzero = nm->mkConst(BitVector(1u, 0u));
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index acb12d649..7b9bdf14f 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -570,19 +570,28 @@ RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){
}
RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) {
- Node resultNode = LinearRewriteStrategy
- < RewriteRule<BVToNatEliminate>
- >::apply(node);
-
- return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ //do not use lazy rewrite strategy if equality solver is disabled
+ if( node[0].isConst() || !options::bitvectorEqualitySolver() ){
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<BVToNatEliminate>
+ >::apply(node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }else{
+ return RewriteResponse(REWRITE_DONE, node);
+ }
}
RewriteResponse TheoryBVRewriter::RewriteIntToBV(TNode node, bool prerewrite) {
- Node resultNode = LinearRewriteStrategy
- < RewriteRule<IntToBVEliminate>
- >::apply(node);
+ //do not use lazy rewrite strategy if equality solver is disabled
+ if( node[0].isConst() || !options::bitvectorEqualitySolver() ){
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<IntToBVEliminate>
+ >::apply(node);
- return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }else{
+ return RewriteResponse(REWRITE_DONE, node);
+ }
}
RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool prerewrite) {
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index cafa7044a..3995aa74f 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -287,6 +287,19 @@ class BitVectorConversionTypeRule {
}
}; /* class BitVectorConversionTypeRule */
+class IntToBitVectorOpTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+
+ if(n.getKind() == kind::INT_TO_BITVECTOR_OP) {
+ size_t bvSize = n.getConst<IntToBitVector>();
+ return nodeManager->mkFunctionType( nodeManager->integerType(), nodeManager->mkBitVectorType(bvSize) );
+ }
+
+ InternalError("bv-conversion typerule invoked for non-bv-conversion kind");
+ }
+}; /* class IntToBitVectorOpTypeRule */
+
class CardinalityComputer {
public:
inline static Cardinality computeCardinality(TypeNode type) {
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index dc3463c84..1210e8495 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -515,6 +515,12 @@ uint64_t numNodes(TNode node, NodeSet& seen);
void collectVariables(TNode node, NodeSet& vars);
+// is bitblast atom
+inline bool isBitblastAtom( Node lit ) {
+ TNode atom = lit.getKind()==kind::NOT ? lit[0] : lit;
+ return atom.getKind()!=kind::EQUAL || atom[0].getType().isBitVector();
+}
+
}
}
}
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 3ef6df3fc..5a99f8e30 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -618,8 +618,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
- std::map< Node, bool > visited;
- collectExtendedFuncTerms( n, visited );
+ d_extt->registerTermRec( n );
}
}
//concat terms do not contribute to theory combination? TODO: verify
@@ -1007,8 +1006,7 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
}
Trace("strings-pending-debug") << " Now collect terms" << std::endl;
//collect extended function terms in the atom
- std::map< Node, bool > visited;
- collectExtendedFuncTerms( atom, visited );
+ d_extt->registerTermRec( atom );
Trace("strings-pending-debug") << " Finished collect terms" << std::endl;
}
@@ -4863,16 +4861,6 @@ Node TheoryStrings::getNormalSymRegExp(Node r, std::vector<Node> &nf_exp) {
return ret;
}
-void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) {
- if( visited.find( n )==visited.end() ){
- visited[n] = true;
- d_extt->registerTerm( n );
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- collectExtendedFuncTerms( n[i], visited );
- }
- }
-}
-
}/* CVC4::theory::strings namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index fd984bd58..6665f9e50 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -278,8 +278,6 @@ private:
bool d_model_active;
};
std::map< Node, ExtfInfoTmp > d_extf_info_tmp;
- //collect extended operator terms
- void collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited );
private:
class InferInfo {
public:
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 9e71a1ddf..1c0a03e9c 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -527,6 +527,21 @@ void ExtTheory::registerTerm( Node n ) {
}
}
+void ExtTheory::registerTermRec( Node n ) {
+ std::map< Node, bool > visited;
+ registerTermRec( n, visited );
+}
+
+void ExtTheory::registerTermRec( Node n, std::map< Node, bool >& visited ) {
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ registerTerm( n );
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ registerTermRec( n[i], visited );
+ }
+ }
+}
+
//mark reduced
void ExtTheory::markReduced( Node n, bool contextDepend ) {
d_ext_func_terms[n] = false;
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 5d64c6446..28552ed79 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -1016,6 +1016,8 @@ protected:
bool doInferencesInternal( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch, bool isRed );
//send lemma
bool sendLemma( Node lem, bool preprocess = false );
+ //register term (recursive)
+ void registerTermRec( Node n, std::map< Node, bool >& visited );
public:
ExtTheory( Theory * p );
virtual ~ExtTheory(){}
@@ -1024,6 +1026,7 @@ public:
//register term
// adds n to d_ext_func_terms if addFunctionKind( n.getKind() ) was called
void registerTerm( Node n );
+ void registerTermRec( Node n );
// set n as reduced/inactive
// if contextDepend = false, then n remains inactive in the duration of this user-context level
void markReduced( Node n, bool contextDepend = true );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback