From e2f28f39b3a3749a5eeed5294f25bec1e210b129 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 11 Nov 2016 12:59:13 -0600 Subject: [PATCH] Add simple inferences for extended bitvector functions, add a few related options. Use bv2nat, int2bv as triggers. Add regressions. --- src/options/bv_options | 6 + src/theory/bv/theory_bv.cpp | 123 ++++++++++++++++-- src/theory/bv/theory_bv.h | 11 +- src/theory/quantifiers/trigger.cpp | 2 +- src/theory/theory_engine.cpp | 8 +- test/regress/regress0/bv/Makefile.am | 6 +- .../regress/regress0/bv/bv-int-collapse1.smt2 | 7 + .../regress0/bv/bv-int-collapse2-sat.smt2 | 8 ++ .../regress/regress0/bv/bv-int-collapse2.smt2 | 7 + .../regress0/bv/bv2nat-simp-range.smt2 | 7 + 10 files changed, 166 insertions(+), 19 deletions(-) create mode 100644 test/regress/regress0/bv/bv-int-collapse1.smt2 create mode 100644 test/regress/regress0/bv/bv-int-collapse2-sat.smt2 create mode 100644 test/regress/regress0/bv/bv-int-collapse2.smt2 create mode 100644 test/regress/regress0/bv/bv2nat-simp-range.smt2 diff --git a/src/options/bv_options b/src/options/bv_options index 341060b37..4a7cbd139 100644 --- a/src/options/bv_options +++ b/src/options/bv_options @@ -72,4 +72,10 @@ expert-option bvIntroducePow2 --bv-intro-pow2 bool :default false option bvLazyRewriteExtf --bv-lazy-rewrite-extf bool :default true :read-write lazily rewrite extended functions like bv2nat and int2bv +option bvLazyReduceExtf --bv-lazy-reduce-extf bool :default false :read-write + reduce extended functions like bv2nat and int2bv at last call instead of full effort + +option bvAlgExtf --bv-alg-extf bool :default true :read-write + algebraic inferences for extended functions + endmodule diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 7bcd23344..869e59502 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -66,7 +66,10 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, d_eagerSolver(NULL), d_abstractionModule(new AbstractionModule(getFullInstanceName())), d_isCoreTheory(false), - d_calledPreregister(false) + d_calledPreregister(false), + d_needsLastCallCheck(false), + d_extf_range_infer(u), + d_extf_collapse_infer(c) { d_extt = new ExtTheory( this ); d_extt->addFunctionKind( kind::BITVECTOR_TO_NAT ); @@ -329,7 +332,7 @@ void TheoryBV::preRegisterTerm(TNode node) { 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 + // AJR : equality solver currently registers all terms to ExtTheory, if we want a lazy reduction without the bv equality solver, need to call this //getExtTheory()->registerTermRec( node ); } @@ -374,9 +377,18 @@ void TheoryBV::checkForLemma(TNode fact) { void TheoryBV::check(Effort e) { - if (done() && !fullEffort(e)) { + if (done() && e nred; + getExtTheory()->getActive( nred ); + doExtfReductions( nred ); + return; + } + TimerStat::CodeTimer checkTimer(d_checkTime); Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer); @@ -460,12 +472,94 @@ void TheoryBV::check(Effort e) if( getExtTheory()->doInferences( 0, nred ) ){ return; } - std::vector< Node > nredr; - if( getExtTheory()->doReductions( 0, nred, nredr ) ){ - return; + d_needsLastCallCheck = false; + if( !nred.empty() ){ + //other inferences involving bv2nat, int2bv + if( options::bvAlgExtf() ){ + if( doExtfInferences( nred ) ){ + return; + } + } + if( !options::bvLazyReduceExtf() ){ + if( doExtfReductions( nred ) ){ + return; + } + }else{ + d_needsLastCallCheck = true; + } + } + } +} + +bool TheoryBV::doExtfInferences( std::vector< Node >& terms ) { + bool sentLemma = false; + eq::EqualityEngine * ee = getEqualityEngine(); + std::map< Node, Node > op_map; + for( unsigned j=0; jmkConst( Rational( 0 ) ); + Node max = NodeManager::currentNM()->mkConst( Rational( Integer(1).multiplyByPow2(bvs) ) ); + Node lem = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, n, min ), NodeManager::currentNM()->mkNode( kind::LT, n, max ) ); + Trace("bv-extf-lemma") << "BV extf lemma (range) : " << lem << std::endl; + d_out->lemma( lem ); + sentLemma = true; + } + } + Node r = ( ee && ee->hasTerm( n[0] ) ) ? ee->getRepresentative( n[0] ) : n[0]; + op_map[r] = n; + } + for( unsigned j=0; jhasTerm( n[0] ) ) ? ee->getRepresentative( n ) : n; + std::map< Node, Node >::iterator it = op_map.find( r ); + if( it!=op_map.end() ){ + Node parent = it->second; + Node cterm = parent[0]==n ? parent : NodeManager::currentNM()->mkNode( parent.getOperator(), n ); + Trace("bv-extf-lemma-debug") << "BV extf collapse based on : " << n << std::endl; + if( d_extf_collapse_infer.find( cterm )==d_extf_collapse_infer.end() ){ + d_extf_collapse_infer.insert( cterm ); + + Node t = n[0]; + if( n.getKind()==kind::INT_TO_BITVECTOR ){ + Assert( t.getType().isInteger() ); + //congruent modulo 2^( bv width ) + unsigned bvs = n.getType().getBitVectorSize(); + Node coeff = NodeManager::currentNM()->mkConst( Rational( Integer(1).multiplyByPow2(bvs) ) ); + Node k = NodeManager::currentNM()->mkSkolem( "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence" ); + t = NodeManager::currentNM()->mkNode( kind::PLUS, t, NodeManager::currentNM()->mkNode( kind::MULT, coeff, k ) ); + } + Node lem = parent.eqNode( t ); + + if( parent[0]!=n ){ + Assert( ee->areEqual( parent[0], n ) ); + lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, parent[0].eqNode( n ), lem ); + } + Trace("bv-extf-lemma") << "BV extf lemma (collapse) : " << lem << std::endl; + d_out->lemma( lem ); + sentLemma = true; + } } - Assert( nredr.empty() ); } + return sentLemma; +} + +bool TheoryBV::doExtfReductions( std::vector< Node >& terms ) { + std::vector< Node > nredr; + if( getExtTheory()->doReductions( 0, terms, nredr ) ){ + return true; + } + Assert( nredr.empty() ); + return false; +} + +bool TheoryBV::needsCheckLastEffort() { + return d_needsLastCallCheck; } void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ @@ -520,18 +614,23 @@ void TheoryBV::propagate(Effort e) { eq::EqualityEngine * TheoryBV::getEqualityEngine() { - return NULL; + CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; + if( core ){ + return core->getEqualityEngine(); + }else{ + return NULL; + } } bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { - CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - if( core ){ + eq::EqualityEngine * ee = getEqualityEngine(); + if( ee ){ //get the constant equivalence classes bool retVal = false; for( unsigned i=0; igetEqualityEngine()->hasTerm( n ) ){ - Node nr = core->getEqualityEngine()->getRepresentative( n ); + if( ee->hasTerm( n ) ){ + Node nr = ee->getRepresentative( n ); if( nr.isConst() ){ subs.push_back( nr ); exp[n].push_back( n.eqNode( nr ) ); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 3cf471356..9973b0736 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -70,6 +70,8 @@ public: void preRegisterTerm(TNode n); void check(Effort e); + + bool needsCheckLastEffort(); void propagate(Effort e); @@ -175,7 +177,14 @@ private: AbstractionModule* d_abstractionModule; bool d_isCoreTheory; bool d_calledPreregister; - + + //for extended functions + bool d_needsLastCallCheck; + context::CDHashSet d_extf_range_infer; + context::CDHashSet d_extf_collapse_infer; + bool doExtfInferences( std::vector< Node >& terms ); + bool doExtfReductions( std::vector< Node >& terms ); + bool wasPropagatedBySubtheory(TNode literal) const { return d_propagatedBy.find(literal) != d_propagatedBy.end(); } diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 3017238ca..7ab9f7065 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -354,7 +354,7 @@ bool Trigger::isAtomicTriggerKind( Kind k ) { return k==APPLY_UF || k==SELECT || k==STORE || k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || - k==SEP_PTO; + k==SEP_PTO || k==BITVECTOR_TO_NAT || k==INT_TO_BITVECTOR; } bool Trigger::isRelationalTrigger( Node n ) { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index cf7611dab..c21aa5445 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -582,6 +582,10 @@ void TheoryEngine::check(Theory::Effort effort) { // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) { + Trace("theory::assertions-model") << endl; + if (Trace.isOn("theory::assertions-model")) { + printAssertions("theory::assertions-model"); + } //checks for theories requiring the model go at last call bool builtModel = false; for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { @@ -607,10 +611,6 @@ void TheoryEngine::check(Theory::Effort effort) { // must build model at this point d_curr_model_builder->buildModel(d_curr_model, true); } - Trace("theory::assertions-model") << endl; - if (Trace.isOn("theory::assertions-model")) { - printAssertions("theory::assertions-model"); - } } } diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index f65fbf9a9..2aeb7a220 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -96,7 +96,11 @@ SMT_TESTS = \ unsound1-reduced.smt2 \ bv2nat-ground.smt2 \ bv2nat-ground-c.smt2 \ - cmu-rdk-3.smt2 + cmu-rdk-3.smt2 \ + bv2nat-simp-range.smt2 \ + bv-int-collapse1.smt2 \ + bv-int-collapse2.smt2 \ + bv-int-collapse2-sat.smt2 # Regression tests for SMT2 inputs SMT2_TESTS = divtest.smt2 diff --git a/test/regress/regress0/bv/bv-int-collapse1.smt2 b/test/regress/regress0/bv/bv-int-collapse1.smt2 new file mode 100644 index 000000000..5b631a7fd --- /dev/null +++ b/test/regress/regress0/bv/bv-int-collapse1.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-fun t () (_ BitVec 16)) +(assert (not (= t ((_ int2bv 16) (bv2nat t))))) +(check-sat) diff --git a/test/regress/regress0/bv/bv-int-collapse2-sat.smt2 b/test/regress/regress0/bv/bv-int-collapse2-sat.smt2 new file mode 100644 index 000000000..1a355a495 --- /dev/null +++ b/test/regress/regress0/bv/bv-int-collapse2-sat.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-fun t () Int) +(assert (> t 0)) +(assert (not (= t (bv2nat ((_ int2bv 16) t))))) +(check-sat) diff --git a/test/regress/regress0/bv/bv-int-collapse2.smt2 b/test/regress/regress0/bv/bv-int-collapse2.smt2 new file mode 100644 index 000000000..a630049cb --- /dev/null +++ b/test/regress/regress0/bv/bv-int-collapse2.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-fun t () Int) +(assert (= (+ t 1) (bv2nat ((_ int2bv 16) t)))) +(check-sat) diff --git a/test/regress/regress0/bv/bv2nat-simp-range.smt2 b/test/regress/regress0/bv/bv2nat-simp-range.smt2 new file mode 100644 index 000000000..e5ea20885 --- /dev/null +++ b/test/regress/regress0/bv/bv2nat-simp-range.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-fun t () (_ BitVec 16)) +(assert (not (and (<= 0 (bv2nat t)) (< (bv2nat t) 65536)))) +(check-sat) -- 2.30.2