From 7c2ea3c85221fce27d8c4d2b7d41a00e103b8cf5 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 12 Aug 2016 12:09:45 -0500 Subject: [PATCH] Minor fixes to model construction to take singleton equivalence classes into account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation. --- src/theory/datatypes/theory_datatypes.cpp | 5 +++++ src/theory/quantifiers/ceg_instantiator.cpp | 13 +++++++----- src/theory/theory_model.cpp | 22 ++++++++++++++------- test/regress/regress0/sets/Makefile.am | 3 ++- test/regress/regress0/sets/dt-simp-mem.smt2 | 9 +++++++++ 5 files changed, 39 insertions(+), 13 deletions(-) create mode 100644 test/regress/regress0/sets/dt-simp-mem.smt2 diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index a2f995935..dc39183b5 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -865,6 +865,11 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ } //d_consEqc[t1] = true; } + //AJR: do this? + //else if( cons2.isConst() ){ + // //prefer the constant + // eqc1->d_constructor = cons2; + //} //d_consEqc[t2] = false; } }else{ diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index cd263e90c..0fe4b98c7 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -749,6 +749,7 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int Trace("cbqi-inst") << pv_coeff << " * "; } Trace("cbqi-inst") << pv << " -> " << n << std::endl; + Assert( n.getType().isSubtypeOf( pv.getType() ) ); } //must ensure variables have been computed for n computeProgVars( n ); @@ -772,6 +773,7 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int std::vector< Node > new_has_coeff; Trace("cbqi-inst-debug2") << "Applying substitutions..." << std::endl; for( unsigned j=0; jfirst].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) ); } } - for( unsigned t=0; t<2; t++ ){ - if( !vts_coeff[t].isNull() ){ - vts_coeff[t] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[t] ) ); - } + //remove delta TODO: check this + vts_coeff[1] = Node::null(); + //multiply inf + if( !vts_coeff[0].isNull() ){ + vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) ); } realPart = real_part.empty() ? d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); Assert( d_out->isEligibleForInstantiation( realPart ) ); @@ -1645,7 +1648,7 @@ int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, No int ires_use = ( msum[pv].isNull() || msum[pv].getConst().sgn()==1 ) ? 1 : -1; val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS, NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ), - NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) ); + NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) ); //TODO: round up for upper bounds? Trace("cbqi-inst-debug") << "result : " << val << std::endl; Assert( val.getType().isInteger() ); } diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index cccd5c350..3cdaeb106 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -375,6 +375,11 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set* } else { if (first) { rep = (*eqc_i); + //add the term (this is specifically for the case of singleton equivalence classes) + if( !rep.getType().isRegExp() ){ + d_equalityEngine->addTerm( rep ); + Trace("model-builder-debug") << "Add term to ee within assertEqualityEngine: " << rep << std::endl; + } first = false; } else { @@ -674,7 +679,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) // Assign representative for this EC if (!const_rep.isNull()) { // Theories should not specify a rep if there is already a constant in the EC - Assert(rep.isNull() || rep == const_rep); + //AJR: I believe this assertion is too strict, eqc with asserted reps may merge with constant eqc + //Assert(rep.isNull() || rep == const_rep); assignConstantRep( tm, constantReps, eqc, const_rep, fullModel ); typeConstSet.add(eqct.getBaseType(), const_rep); } @@ -812,14 +818,16 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) //get properties of this type bool isCorecursive = false; - bool isUSortFiniteRestricted = false; if( t.isDatatype() ){ const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype(); isCorecursive = dt.isCodatatype() && ( !dt.isFinite() || dt.isRecursiveSingleton() ); } +#ifdef CVC4_ASSERTIONS + bool isUSortFiniteRestricted = false; if( options::finiteModelFind() ){ isUSortFiniteRestricted = !t.isSort() && involvesUSort( t ); } +#endif set* repSet = typeRepSet.getSet(t); TypeNode tb = t.getBaseType(); @@ -864,8 +872,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Assert( !n.isNull() ); success = true; Trace("model-builder-debug") << "Check if excluded : " << n << std::endl; - if( isUSortFiniteRestricted ){ #ifdef CVC4_ASSERTIONS + if( isUSortFiniteRestricted ){ //must not involve uninterpreted constants beyond cardinality bound (which assumed to coincide with #eqc) //this is just an assertion now, since TypeEnumeratorProperties should ensure that only legal values are enumerated wrt this constraint. std::map< Node, bool > visited; @@ -874,8 +882,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Trace("model-builder") << "Excluded value for " << t << " : " << n << " due to out of range uninterpreted constant." << std::endl; } Assert( success ); -#endif } +#endif if( success && isCorecursive ){ if (repSet != NULL && !repSet->empty()) { // in the case of codatatypes, check if it is in the set of values that we cannot assign @@ -960,9 +968,9 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) //modelBuilder-specific initialization processBuildModel( tm, fullModel ); - // Collect model comments from the theories + // Do post-processing of model from the theories (used for THEORY_SEP to construct heap model) if( fullModel ){ - Trace("model-builder") << "TheoryEngineModelBuilder: Collect model comments..." << std::endl; + Trace("model-builder") << "TheoryEngineModelBuilder: Post-process model..." << std::endl; d_te->postProcessModel(tm); } @@ -1044,7 +1052,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node retNode = NodeManager::currentNM()->mkNode( r.getKind(), children ); if (childrenConst) { retNode = Rewriter::rewrite(retNode); - Assert(retNode.getKind()==kind::APPLY_UF || retNode.getKind()==kind::REGEXP_RANGE || retNode.isConst()); + Assert(retNode.getKind()==kind::APPLY_UF || retNode.getType().isRegExp() || retNode.isConst()); } } d_normalizedCache[r] = retNode; diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 19f6313fb..98e7e744c 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -62,7 +62,8 @@ TESTS = \ union-1a.smt2 \ union-1b-flip.smt2 \ union-1b.smt2 \ - union-2.smt2 + union-2.smt2 \ + dt-simp-mem.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/dt-simp-mem.smt2 b/test/regress/regress0/sets/dt-simp-mem.smt2 new file mode 100644 index 000000000..a38544aa2 --- /dev/null +++ b/test/regress/regress0/sets/dt-simp-mem.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-datatypes () ((D (A (a Int))))) +(declare-fun x1 () D) +(declare-fun S () (Set D)) +(declare-fun P (D) Bool) +(assert (member x1 S)) +(assert (=> (member (A 0) S) (P x1))) +(check-sat) -- 2.30.2