From: ajreynol Date: Sat, 18 Oct 2014 11:37:36 +0000 (+0200) Subject: Fix for bounded integers when incremental, fixes bug 588. Add option --dt-binary... X-Git-Tag: cvc5-1.0.0~6553 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d376e1e960617cdea19759f36babfd1f88e37e6d;p=cvc5.git Fix for bounded integers when incremental, fixes bug 588. Add option --dt-binary-split. --- diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options index 7e56b4d7a..bc7552862 100644 --- a/src/theory/datatypes/options +++ b/src/theory/datatypes/options @@ -13,6 +13,8 @@ expert-option dtRewriteErrorSel --dt-rewrite-error-sel bool :default false rewrite incorrectly applied selectors to arbitrary ground term option dtForceAssignment --dt-force-assignment bool :default false :read-write force the datatypes solver to give specific values to all datatypes terms before answering sat +option dtBinarySplit --dt-binary-split bool :default false + do binary splits for datatype constructor types option cdtBisimilar --cdt-bisimilar bool :default true do bisimilarity check for co-datatypes diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index f717e7701..b7e2e5eb3 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -222,14 +222,25 @@ void TheoryDatatypes::check(Effort e) { Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl; d_infer.push_back( t ); }else{ - Trace("dt-split") << "*************Split for constructors on " << n << endl; - std::vector< Node > children; - for( unsigned i=0; imkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n ); - children.push_back( test ); + if( options::dtBinarySplit() ){ + Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n ); + Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; + test = Rewriter::rewrite( test ); + NodeBuilder<> nb(kind::OR); + nb << test << test.notNode(); + Node lemma = nb; + d_out->lemma( lemma ); + d_out->requirePhase( test, true ); + }else{ + Trace("dt-split") << "*************Split for constructors on " << n << endl; + std::vector< Node > children; + for( unsigned i=0; imkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n ); + children.push_back( test ); + } + Node lemma = NodeManager::currentNM()->mkNode( kind::OR, children ); + d_out->lemma( lemma ); } - Node lemma = NodeManager::currentNM()->mkNode( kind::OR, children ); - d_out->lemma( lemma ); return; } }else{ diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 57799fd8e..91c04bc80 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -28,8 +28,8 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; -BoundedIntegers::RangeModel::RangeModel(BoundedIntegers * bi, Node r, context::Context* c, bool isProxy) : d_bi(bi), - d_range(r), d_curr_max(-1), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1) { +BoundedIntegers::RangeModel::RangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy) : d_bi(bi), + d_range(r), d_curr_max(-1), d_lit_to_range(u), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1), d_ranges_proxied(u) { if( options::fmfBoundIntLazy() ){ d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() ); }else{ @@ -59,17 +59,18 @@ void BoundedIntegers::RangeModel::assertNode(Node n) { bool pol = n.getKind()!=NOT; Node nlit = n.getKind()==NOT ? n[0] : n; if( d_lit_to_range.find( nlit )!=d_lit_to_range.end() ){ + int vrange = d_lit_to_range[nlit]; Trace("bound-int-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")"; Trace("bound-int-assert") << ", found literal " << nlit; - Trace("bound-int-assert") << ", it is bound literal " << d_lit_to_range[nlit] << " for " << d_range << std::endl; + Trace("bound-int-assert") << ", it is bound literal " << vrange << " for " << d_range << std::endl; d_range_assertions[nlit] = (pol==d_lit_to_pol[nlit]); if( pol!=d_lit_to_pol[nlit] ){ //check if we need a new split? if( !d_has_range ){ bool needsRange = true; - for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){ - if( d_range_assertions.find( it->first )==d_range_assertions.end() ){ - Trace("bound-int-debug") << "Does not need range because of " << it->first << std::endl; + for( NodeIntMap::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){ + if( d_range_assertions.find( (*it).first )==d_range_assertions.end() ){ + Trace("bound-int-debug") << "Does not need range because of " << (*it).first << std::endl; needsRange = false; break; } @@ -79,9 +80,9 @@ void BoundedIntegers::RangeModel::assertNode(Node n) { } } }else{ - if (!d_has_range || d_lit_to_range[nlit]::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){ - int i = it->second; + for( NodeIntMap::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){ + int i = (*it).second; if( !d_has_range || ifirst; + Node rn = (*it).first; Assert( !rn.isNull() ); if( d_range_assertions.find( rn )==d_range_assertions.end() ){ - if (!d_lit_to_pol[it->first]) { + if (!d_lit_to_pol[rn]) { rn = rn.negate(); } Trace("bound-int-dec-debug") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl; @@ -335,7 +336,7 @@ void BoundedIntegers::registerQuantifier( Node f ) { if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){ Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << " " << r.getKind() << std::endl; d_ranges.push_back( r ); - d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext(), isProxy ); + d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext(), d_quantEngine->getUserContext(), isProxy ); d_rms[r]->initialize(); } } diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index 355360e41..c09527f89 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -38,6 +38,7 @@ class BoundedIntegers : public QuantifiersModule typedef context::CDHashMap NodeBoolMap; typedef context::CDHashMap NodeIntMap; typedef context::CDHashMap NodeNodeMap; + typedef context::CDHashMap IntBoolMap; private: //for determining bounds bool isBound( Node f, Node v ); @@ -62,16 +63,16 @@ private: void allocateRange(); Node d_proxy_range; public: - RangeModel(BoundedIntegers * bi, Node r, context::Context* c, bool isProxy); + RangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy); Node d_range; int d_curr_max; std::map< int, Node > d_range_literal; std::map< Node, bool > d_lit_to_pol; - std::map< Node, int > d_lit_to_range; + NodeIntMap d_lit_to_range; NodeBoolMap d_range_assertions; context::CDO< bool > d_has_range; context::CDO< int > d_curr_range; - std::map< int, bool > d_ranges_proxied; + IntBoolMap d_ranges_proxied; void initialize(); void assertNode(Node n); Node getNextDecisionRequest();