From 9da056f71c0c4a8ed5afd01c300e9c86cfcf5601 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 13 Oct 2016 17:44:19 -0500 Subject: [PATCH] Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory. --- src/theory/bv/aig_bitblaster.cpp | 1 + src/theory/bv/bv_subtheory_bitblast.cpp | 17 ++++- src/theory/bv/bv_subtheory_core.cpp | 11 ++++ src/theory/bv/bv_subtheory_core.h | 5 +- src/theory/bv/bv_subtheory_inequality.cpp | 16 +++-- src/theory/bv/eager_bitblaster.cpp | 2 + src/theory/bv/kinds | 1 + src/theory/bv/lazy_bitblaster.cpp | 11 +++- src/theory/bv/theory_bv.cpp | 66 ++++++++++++++++++- src/theory/bv/theory_bv.h | 1 + ...ry_bv_rewrite_rules_operator_elimination.h | 8 +++ src/theory/bv/theory_bv_rewriter.cpp | 27 +++++--- src/theory/bv/theory_bv_type_rules.h | 13 ++++ src/theory/bv/theory_bv_utils.h | 6 ++ src/theory/strings/theory_strings.cpp | 16 +---- src/theory/strings/theory_strings.h | 2 - src/theory/theory.cpp | 15 +++++ src/theory/theory.h | 3 + test/regress/regress0/bv/bv2nat-ground-c.smt2 | 15 +++++ test/regress/regress0/bv/bv2nat-ground.smt2 | 16 +++++ test/regress/regress0/bv/cmu-rdk-3.smt2 | 9 +++ 21 files changed, 221 insertions(+), 40 deletions(-) create mode 100644 test/regress/regress0/bv/bv2nat-ground-c.smt2 create mode 100644 test/regress/regress0/bv/bv2nat-ground.smt2 create mode 100644 test/regress/regress0/bv/cmu-rdk-3.smt2 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 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; igetEqualityEngine()->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().size; + NodeManager* const nm = NodeManager::currentNM(); + const Node bvzero = nm->mkConst(BitVector(1u, 0u)); + const Node bvone = nm->mkConst(BitVector(1u, 1u)); + std::vector 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::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << 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::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + //if( node[0].isConst() ){ + //TODO? direct computation instead of term construction+rewriting + //} + const unsigned size = node.getOperator().getConst().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 - >::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 + >::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 - >::apply(node); + //do not use lazy rewrite strategy if equality solver is disabled + if( node[0].isConst() || !options::bitvectorEqualitySolver() ){ + Node resultNode = LinearRewriteStrategy + < RewriteRule + >::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(); + 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 &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 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& 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 ); diff --git a/test/regress/regress0/bv/bv2nat-ground-c.smt2 b/test/regress/regress0/bv/bv2nat-ground-c.smt2 new file mode 100644 index 000000000..2bb09c2cf --- /dev/null +++ b/test/regress/regress0/bv/bv2nat-ground-c.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_BVLIA) +(set-info :status unsat) +(declare-const a (_ BitVec 32)) +(declare-const b (_ BitVec 32)) +(declare-const c (_ BitVec 32)) +(declare-const d (_ BitVec 32)) +(declare-const e (_ BitVec 32)) + +(assert (or (= a #x00000007) (= a #x00000005) (= a #x00000100))) + +(assert (not (= (bv2nat a) 7))) +(assert (not (= (bv2nat a) 5))) +(assert (< (bv2nat a) 10)) + +(check-sat) diff --git a/test/regress/regress0/bv/bv2nat-ground.smt2 b/test/regress/regress0/bv/bv2nat-ground.smt2 new file mode 100644 index 000000000..f72228b28 --- /dev/null +++ b/test/regress/regress0/bv/bv2nat-ground.smt2 @@ -0,0 +1,16 @@ +(set-logic QF_BVLIA) +(set-info :status unsat) +(declare-const a (_ BitVec 32)) +(declare-const b (_ BitVec 32)) +(declare-const c (_ BitVec 32)) +(declare-const d (_ BitVec 32)) +(declare-const e (_ BitVec 32)) + +(assert (or (= a b) (= a c) (= a d) (= a e))) + +(assert (not (= (bv2nat a) (bv2nat b)))) +(assert (not (= (bv2nat a) (bv2nat c)))) +(assert (not (= (bv2nat a) (bv2nat d)))) +(assert (not (= (bv2nat a) (bv2nat e)))) + +(check-sat) diff --git a/test/regress/regress0/bv/cmu-rdk-3.smt2 b/test/regress/regress0/bv/cmu-rdk-3.smt2 new file mode 100644 index 000000000..742dd593b --- /dev/null +++ b/test/regress/regress0/bv/cmu-rdk-3.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-fun y () Int) +(declare-fun x () Int) + +(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (= (bv2nat (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))))))) ((_ int2bv 3) 1))) 0) 1 0) 0)))) (not (= (ite (>= x 0) 1 0) 0))) (not (= (ite (>= y 0) 1 0) 0))) (not (= (ite (= x y) 1 0) 0))) (not (not (= (ite (= x 0) 1 0) 0)))) (not (not (= (ite (= y 0) 1 0) 0)))) (not (= (ite (= (bv2nat (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x)))) ((_ int2bv 3) 1))) 0) 1 0) 0))) (and (= x (bv2nat ((_ int2bv 3) x))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))) (_ bv0 1))) (and (= y (bv2nat ((_ int2bv 3) y))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvashr ((_ int2bv 3) y) ((_ int2bv 3) 1))) (_ bv0 1))) (and (= (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))) (bv2nat ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))) (= (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))) (bv2nat ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))))) (= ((_ extract 0 0) (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))) (_ bv0 1))) (and (= (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))) (bv2nat ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))))))))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))))))) ((_ int2bv 3) 1))) (_ bv0 1))) (and (= x (bv2nat ((_ int2bv 3) x))) (= x (bv2nat ((_ int2bv 3) x))))) (= ((_ extract 0 0) (bvor ((_ int2bv 3) x) ((_ int2bv 3) x))) (_ bv0 1))) (and (= (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x))) (bv2nat ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x)))))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x)))) ((_ int2bv 3) 1))) (_ bv0 1)))) + +(check-sat) -- 2.30.2