From 2150eb22aaff94f9d0d9f0ee0854ea44675fd854 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 19 Feb 2016 11:00:48 -0600 Subject: [PATCH] Fixes and improvements for datatypes properties and splitting. --- src/expr/datatype.cpp | 20 ++++++++++++++----- src/theory/quantifiers/quant_split.cpp | 17 ++++++++++------ src/theory/quantifiers_engine.cpp | 10 +++++----- test/regress/regress0/fmf/Makefile.am | 3 ++- .../fmf/datatypes-ufinite-nested.smt2 | 17 ++++++++++++++++ .../regress0/fmf/datatypes-ufinite.smt2 | 6 +++--- 6 files changed, 53 insertions(+), 20 deletions(-) create mode 100644 test/regress/regress0/fmf/datatypes-ufinite-nested.smt2 diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 45a7447aa..b52ceb856 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -306,10 +306,11 @@ bool Datatype::isUFinite() const throw(IllegalArgumentException) { if(self.getAttribute(DatatypeUFiniteComputedAttr())) { return self.getAttribute(DatatypeUFiniteAttr()); } + //start by assuming it is not + self.setAttribute(DatatypeUFiniteComputedAttr(), true); + self.setAttribute(DatatypeUFiniteAttr(), false); for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { if(! (*i).isUFinite()) { - self.setAttribute(DatatypeUFiniteComputedAttr(), true); - self.setAttribute(DatatypeUFiniteAttr(), false); return false; } } @@ -838,7 +839,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { return self.getAttribute(DatatypeFiniteAttr()); } for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - if(! SelectorType((*i).getSelector().getType()).getRangeType().getCardinality().isFinite()) { + if(! (*i).getRangeType().getCardinality().isFinite()) { self.setAttribute(DatatypeFiniteComputedAttr(), true); self.setAttribute(DatatypeFiniteAttr(), false); return false; @@ -858,9 +859,18 @@ bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) { if(self.getAttribute(DatatypeUFiniteComputedAttr())) { return self.getAttribute(DatatypeUFiniteAttr()); } + bool success = true; for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - Type t = SelectorType((*i).getSelector().getType()).getRangeType(); - if(!t.isSort() && !t.getCardinality().isFinite()) { + Type t = (*i).getRangeType(); + if( t.isDatatype() ){ + const Datatype& dt = ((DatatypeType)t).getDatatype(); + if( !dt.isUFinite() ){ + success = false; + } + }else if(!t.isSort() && !t.getCardinality().isFinite()) { + success = false; + } + if(!success ){ self.setAttribute(DatatypeUFiniteComputedAttr(), true); self.setAttribute(DatatypeUFiniteAttr(), false); return false; diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index e874ee5b8..1ae1c3c5f 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -48,11 +48,11 @@ void QuantDSplit::preRegisterQuantifier( Node q ) { }else{ int score = -1; if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ - score = dt.isFinite() ? 1 : -1; - }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){ + score = dt.isUFinite() ? 1 : -1; + }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){ score = dt.isUFinite() ? 1 : -1; } - Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << std::endl; + Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isUFinite() << " " << dt.isFinite() << ")" << std::endl; if( score>max_score ){ max_index = i; max_score = score; @@ -70,11 +70,12 @@ void QuantDSplit::preRegisterQuantifier( Node q ) { /* whether this module needs to check this round */ bool QuantDSplit::needsCheck( Theory::Effort e ) { - return e>=Theory::EFFORT_FULL; + return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty(); } + /* Call during quantifier engine's check */ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) { - //flush lemmas ASAP (they are a reduction) + //add lemmas ASAP (they are a reduction) if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){ std::vector< Node > lemmas; for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) { @@ -92,6 +93,7 @@ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) { TNode svar = q[0][it->second]; TypeNode tn = svar.getType(); if( tn.isDatatype() ){ + std::vector< Node > cons; const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); for( unsigned j=0; j vars; @@ -110,8 +112,10 @@ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) { if( !bvs_cmb.empty() ){ body = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bvs_cmb ), body ); } - disj.push_back( body ); + cons.push_back( body ); } + Node conc = cons.size()==1 ? cons[0] : NodeManager::currentNM()->mkNode( kind::AND, cons ); + disj.push_back( conc ); }else{ Assert( false ); } @@ -124,6 +128,7 @@ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) { Trace("quant-dsplit") << "QuantDSplit lemma : " << lemmas[i] << std::endl; d_quantEngine->addLemma( lemmas[i], false ); } + d_quant_to_reduce.clear(); } } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index cfb3fda94..bbc41278e 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -241,7 +241,7 @@ void QuantifiersEngine::finishInit(){ d_modules.push_back( d_lte_part_inst ); } if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) || - options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_AGG ){ + options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ d_qsplit = new quantifiers::QuantDSplit( this, c ); d_modules.push_back( d_qsplit ); } @@ -365,10 +365,10 @@ void QuantifiersEngine::check( Theory::Effort e ){ } bool usedModelBuilder = false; - Trace("quant-engine-debug") << "Quantifiers Engine call to check, level = " << e << std::endl; + Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl; if( needsCheck ){ - Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl; if( Trace.isOn("quant-engine-debug") ){ + Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl; Trace("quant-engine-debug") << " modules to check : "; for( unsigned i=0; iidentify() << " "; @@ -484,9 +484,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } } - Trace("quant-engine") << "Finished quantifiers engine check." << std::endl; + Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl; }else{ - Trace("quant-engine") << "Quantifiers Engine does not need check." << std::endl; + Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl; } //SAT case diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index a3ff2fcc7..aa3508798 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -51,7 +51,8 @@ TESTS = \ fmc_unsound_model.smt2 \ am-bad-model.cvc \ nun-0208-to.smt2 \ - datatypes-ufinite.smt2 + datatypes-ufinite.smt2 \ + datatypes-ufinite-nested.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2 b/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2 new file mode 100644 index 000000000..3ffc36d05 --- /dev/null +++ b/test/regress/regress0/fmf/datatypes-ufinite-nested.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-sort U 0) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) +(declare-fun d () U) +(assert (distinct a b c)) +(declare-sort V 0) +(declare-datatypes () ((ufin1 (cons1 (s11 U) (s13 ufin2))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3)))) +(declare-fun P (ufin1 ufin2) Bool) +(declare-fun Q (ufin1 ufin1) Bool) +(assert (forall ((x ufin1) (y ufin2) (z ufin1)) (or (P x y) (Q x z)))) +(assert (not (P (cons1 a cons3) cons3))) +(assert (not (Q (cons1 b cons3) (cons1 a cons3)))) +(check-sat) diff --git a/test/regress/regress0/fmf/datatypes-ufinite.smt2 b/test/regress/regress0/fmf/datatypes-ufinite.smt2 index d802930fd..3564bff8b 100644 --- a/test/regress/regress0/fmf/datatypes-ufinite.smt2 +++ b/test/regress/regress0/fmf/datatypes-ufinite.smt2 @@ -8,10 +8,10 @@ (declare-fun d () U) (assert (distinct a b c)) (declare-sort V 0) -(declare-datatypes () ((ufin1 (cons1 (s11 U) (s12 U) (s13 U))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3)))) +(declare-datatypes () ((ufin1 (cons1 (s11 U) (s12 U))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3)))) (declare-fun P (ufin1 ufin2) Bool) (declare-fun Q (ufin1 ufin1) Bool) (assert (forall ((x ufin1) (y ufin2) (z ufin1)) (or (P x y) (Q x z)))) -(assert (not (P (cons1 a a a) cons3))) -(assert (not (Q (cons1 a d a) (cons1 a b c)))) +(assert (not (P (cons1 a a) cons3))) +(assert (not (Q (cons1 a d) (cons1 a b)))) (check-sat) -- 2.30.2