From c431410d0bd4a688d5d446f906d80634424dcd53 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Apr 2014 10:31:47 -0500 Subject: Add support for cardinality constraints logic UFC. Add regressions in fmf/. Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit. --- src/parser/smt1/smt1.h | 3 +- src/smt/smt_engine.cpp | 19 +-- src/theory/datatypes/theory_datatypes.cpp | 128 ++++++++++++--------- src/theory/logic_info.cpp | 10 ++ src/theory/logic_info.h | 6 + src/theory/quantifiers/first_order_model.cpp | 5 +- src/theory/quantifiers/modes.cpp | 7 +- src/theory/quantifiers/modes.h | 6 +- src/theory/quantifiers/options | 4 +- src/theory/quantifiers/options_handlers.h | 18 +-- src/theory/quantifiers/term_database.cpp | 2 +- src/theory/uf/theory_uf.cpp | 7 +- src/util/datatype.cpp | 21 +++- src/util/datatype.h | 8 +- test/regress/regress0/bug512.smt2 | 2 +- .../regress0/fmf/Arrow_Order-smtlib.778341.smt | 2 +- test/regress/regress0/fmf/Makefile.am | 11 +- test/regress/regress0/fmf/QEpres-uf.855035.smt | 2 +- test/regress/regress0/fmf/fc-pigeonhole19.smt2 | 20 ++++ test/regress/regress0/fmf/fc-simple.smt2 | 12 ++ test/regress/regress0/fmf/fc-unsat-pent.smt2 | 20 ++++ test/regress/regress0/fmf/fc-unsat-tot-2.smt2 | 14 +++ test/regress/regress0/quantifiers/bug269.smt2 | 2 + test/regress/regress0/quantifiers/burns13.smt2 | 2 + test/regress/regress0/rewriterules/Makefile.am | 6 +- test/regress/regress0/rewriterules/read5.smt2 | 35 ++++++ test/regress/regress0/tptp/Makefile.am | 2 +- 27 files changed, 277 insertions(+), 97 deletions(-) create mode 100755 test/regress/regress0/fmf/fc-pigeonhole19.smt2 create mode 100755 test/regress/regress0/fmf/fc-simple.smt2 create mode 100755 test/regress/regress0/fmf/fc-unsat-pent.smt2 create mode 100755 test/regress/regress0/fmf/fc-unsat-tot-2.smt2 create mode 100755 test/regress/regress0/rewriterules/read5.smt2 diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h index f96a4e810..c19b0f872 100644 --- a/src/parser/smt1/smt1.h +++ b/src/parser/smt1/smt1.h @@ -84,7 +84,8 @@ public: THEORY_REALS, THEORY_REALS_INTS, THEORY_STRINGS, - THEORY_QUANTIFIERS + THEORY_QUANTIFIERS, + THEORY_CARDINALITY_CONSTRAINT }; private: diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8586bc9da..36f9866f4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1112,7 +1112,7 @@ void SmtEngine::setDefaults() { if(!options::decisionMode.wasSetByUser()) { decision::DecisionMode decMode = // ALL_SUPPORTED - d_logic.hasEverything() ? decision::DECISION_STRATEGY_INTERNAL : + d_logic.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION : ( // QF_BV (not d_logic.isQuantified() && d_logic.isPure(THEORY_BV) @@ -1153,9 +1153,7 @@ void SmtEngine::setDefaults() { // QF_LRA (not d_logic.isQuantified() && d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed() - ) || - // Quantifiers - d_logic.isQuantified() + ) ? true : false ); @@ -1172,12 +1170,17 @@ void SmtEngine::setDefaults() { options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } } - if ( options::fmfBoundInt() ){ + if( d_logic.hasCardinalityConstraints() ){ + //must have finite model finding on + options::finiteModelFind.set( true ); + } + if( options::fmfBoundInt() ){ //must have finite model finding on options::finiteModelFind.set( true ); - if( options::mbqiMode()!=quantifiers::MBQI_NONE && - options::mbqiMode()!=quantifiers::MBQI_FMC && - options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ){ + if( ! options::mbqiMode.wasSetByUser() || + ( options::mbqiMode()!=quantifiers::MBQI_NONE && + options::mbqiMode()!=quantifiers::MBQI_FMC && + options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ) ){ //if bounded integers are set, use no MBQI by default options::mbqiMode.set( quantifiers::MBQI_NONE ); } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 0c6842222..b00b4148d 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -889,14 +889,48 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Trace("dt-model") << std::endl; printModelDebug( "dt-model" ); Trace("dt-model") << std::endl; + + /* + bool eq_merged = false; + std::vector< Node > all_eqc; + eq::EqClassesIterator eqcs1_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs1_i.isFinished() ){ + Node eqc = (*eqcs1_i); + all_eqc.push_back( eqc ); + ++eqcs1_i; + } + //check if equivalence classes have merged + for( unsigned i=0; iareEqual( all_eqc[i], all_eqc[j] ) ){ + Trace("dt-cmi") << "Pre-already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl; + eq_merged = true; + } + } + } + Assert( !eq_merged ); + */ + + //combine the equality engine m->assertEqualityEngine( &d_equalityEngine ); -/* - std::vector< TypeEnumerator > vec; - std::map< TypeNode, int > tes; + + /* + //check again if equivalence classes have merged + for( unsigned i=0; iareEqual( all_eqc[i], all_eqc[j] ) ){ + Trace("dt-cmi") << "Already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl; + eq_merged = true; + } + } + } + Assert( !eq_merged ); */ + //get all constructors eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine ); std::vector< Node > cons; + std::vector< Node > nodes; while( !eqccs_i.isFinished() ){ Node eqc = (*eqccs_i); //for all equivalence classes that are datatypes @@ -904,28 +938,13 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); if( !ei->d_constructor.get().isNull() ){ cons.push_back( ei->d_constructor.get() ); - } - } - ++eqccs_i; - } - - //must choose proper representatives - std::vector< Node > nodes; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - //for all equivalence classes that are datatypes - if( DatatypesRewriter::isTermDatatype( eqc ) ){ - EqcInfo* ei = getOrMakeEqcInfo( eqc ); - if( !ei->d_constructor.get().isNull() ){ - //specify that we should use the constructor as the representative - //m->assertRepresentative( ei->d_constructor.get() ); }else{ nodes.push_back( eqc ); } } - ++eqcs_i; + ++eqccs_i; } + unsigned index = 0; while( indexareEqual( cons[i][j], n[j] ) ){ - diff = true; - break; - } - } - if( !diff ){ - Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; - success = false; - break; - } - } - } - }else{ - Trace("dt-cmi-debug") << "...Not consistent with labels" << std::endl; - success = false; + std::map< int, std::map< int, bool > > sels; + Trace("dt-cmi") << "Existing selectors : "; + NodeListMap::iterator sel_i = d_selector_apps.find( eqc ); + if( sel_i != d_selector_apps.end() ){ + NodeList* sel = (*sel_i).second; + for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){ + Expr selectorExpr = (*j).getOperator().toExpr(); + unsigned cindex = Datatype::cindexOf( selectorExpr ); + unsigned index = Datatype::indexOf( selectorExpr ); + sels[cindex][index] = true; + Trace("dt-cmi") << (*j) << " (" << cindex << ", " << index << ") "; } - }while( !success ); + } + Trace("dt-cmi") << std::endl; */ + const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); for( unsigned r=0; r<2; r++ ){ if( neqc.isNull() ){ @@ -1017,6 +1014,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ if( pcons[i] && (r==1)==dt[ i ].isFinite() ){ neqc = getInstantiateCons( eqc, dt, i, false, false ); for( unsigned j=0; jassertEquality( eqc, neqc, true ); + /* + for( unsigned kk=0; kkareEqual( all_eqc[kk], all_eqc[ll] ) ){ + Trace("dt-cmi") << "Forced equal : " << kk << " " << ll << " : " << all_eqc[kk] << " = " << all_eqc[ll] << std::endl; + Node r = m->getRepresentative( all_eqc[kk] ); + Trace("dt-cmi") << " { "; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, m->d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Trace("dt-cmi") << (*eqc_i) << " "; + ++eqc_i; + } + Trace("dt-cmi") << "} " << std::endl; + } + Assert( !m->areEqual( all_eqc[kk], all_eqc[ll] ) ); + } + } + */ //m->assertRepresentative( neqc ); cons.push_back( neqc ); ++index; diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index c079eecf9..78f4996b8 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -37,6 +37,7 @@ LogicInfo::LogicInfo() : d_reals(true), d_linear(true),// for now, "everything enabled" doesn't include non-linear arith d_differenceLogic(false), + d_cardinalityConstraints(false), d_locked(false) { for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { @@ -52,6 +53,7 @@ LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) : d_reals(false), d_linear(false), d_differenceLogic(false), + d_cardinalityConstraints(false), d_locked(false) { setLogicString(logicString); @@ -66,6 +68,7 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : d_reals(false), d_linear(false), d_differenceLogic(false), + d_cardinalityConstraints(false), d_locked(false) { setLogicString(logicString); @@ -97,6 +100,9 @@ std::string LogicInfo::getLogicString() const { ss << "UF"; ++seen; } + if( d_cardinalityConstraints ){ + ss << "C"; + } if(d_theories[THEORY_BV]) { ss << "BV"; ++seen; @@ -191,6 +197,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc enableTheory(THEORY_UF); p += 2; } + if(!strncmp(p, "C", 1 )) { + d_cardinalityConstraints = true; + p += 1; + } // allow BV or DT in either order if(!strncmp(p, "BV", 2)) { enableTheory(THEORY_BV); diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index a0777ae70..1c4b69b15 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -52,6 +52,7 @@ class CVC4_PUBLIC LogicInfo { bool d_reals; /**< are reals used in this logic? */ bool d_linear; /**< linear-only arithmetic in this logic? */ bool d_differenceLogic; /**< difference-only arithmetic in this logic? */ + bool d_cardinalityConstraints; /**< cardinality constraints in this logic? */ bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */ @@ -175,6 +176,11 @@ public: CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic"); return d_differenceLogic; } + /** Does this logic allow cardinality constraints? */ + bool hasCardinalityConstraints() const { + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + return d_cardinalityConstraints; + } // MUTATORS diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index f3203da4b..54be11b44 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -656,6 +656,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { Node cond = d_models[op]->d_cond[i]; std::vector< Node > children; for( unsigned j=0; jmkNode( GEQ, vars[j], cond[j][0] ) ); @@ -663,7 +664,8 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { if( !isStar(cond[j][1]) ){ children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) ); } - }else if (!isStar(cond[j])){ + }else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground representatives of this type... + d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){ Node c = getUsedRepresentative( cond[j] ); children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) ); } @@ -673,6 +675,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr ); } } + Trace("fmc-model") << "Made " << curr << " for " << op << std::endl; curr = Rewriter::rewrite( curr ); return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); } diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp index 10185914e..8bd97a8a7 100644 --- a/src/theory/quantifiers/modes.cpp +++ b/src/theory/quantifiers/modes.cpp @@ -79,8 +79,8 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::AxiomInstMode m std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) { switch(mode) { - case theory::quantifiers::MBQI_DEFAULT: - out << "MBQI_DEFAULT"; + case theory::quantifiers::MBQI_GEN_EVAL: + out << "MBQI_GEN_EVAL"; break; case theory::quantifiers::MBQI_NONE: out << "MBQI_NONE"; @@ -94,6 +94,9 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) case theory::quantifiers::MBQI_INTERVAL: out << "MBQI_INTERVAL"; break; + case theory::quantifiers::MBQI_TRUST: + out << "MBQI_TRUST"; + break; default: out << "MbqiMode!UNKNOWN"; } diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 89e10b175..80534c8b0 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -58,13 +58,13 @@ typedef enum { } AxiomInstMode; typedef enum { - /** default, mbqi from CADE 24 paper */ - MBQI_DEFAULT, + /** mbqi from CADE 24 paper */ + MBQI_GEN_EVAL, /** no mbqi */ MBQI_NONE, /** implementation that mimics inst-gen */ MBQI_INST_GEN, - /** mbqi from Section 5.4.2 of AJR thesis */ + /** default, mbqi from Section 5.4.2 of AJR thesis */ MBQI_FMC, /** mbqi with integer intervals */ MBQI_FMC_INTERVAL, diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 0865f2c0b..b7f015f47 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -71,7 +71,7 @@ option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :de option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly -option fullSaturateQuant --full-saturate-quant bool :default true +option fullSaturateQuant --full-saturate-quant bool :default false when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" @@ -95,7 +95,7 @@ option internalReps /--disable-quant-internal-reps bool :default true option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write use finite model finding heuristic for quantifier instantiation -option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" +option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" choose mode for model-based quantifier instantiation option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false only add one instantiation per quantifier per round for mbqi diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index e9c754d4a..164e9e643 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -82,8 +82,8 @@ static const std::string mbqiModeHelp = "\ Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ \n\ default \n\ -+ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\ - model finding paper.\n\ ++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\ + Modulo Theories.\n\ \n\ none \n\ + Disable model-based quantifier instantiation.\n\ @@ -91,12 +91,12 @@ none \n\ instgen \n\ + Use instantiation algorithm that mimics Inst-Gen calculus. \n\ \n\ -fmc \n\ -+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\ - Modulo Theories.\n\ +gen-ev \n\ ++ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\ + model finding paper.\n\ \n\ fmc-interval \n\ -+ Same as fmc, but with intervals for models of integer functions.\n\ ++ Same as default, but with intervals for models of integer functions.\n\ \n\ interval \n\ + Use algorithm that abstracts domain elements as intervals. \n\ @@ -217,13 +217,13 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar } inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default") { - return MBQI_DEFAULT; + if(optarg == "gen-ev") { + return MBQI_GEN_EVAL; } else if(optarg == "none") { return MBQI_NONE; } else if(optarg == "instgen") { return MBQI_INST_GEN; - } else if(optarg == "fmc") { + } else if(optarg == "default" || optarg == "fmc") { return MBQI_FMC; } else if(optarg == "fmc-interval") { return MBQI_FMC_INTERVAL; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index ea1231e7a..e6ee8f53b 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -81,7 +81,7 @@ Node TermDb::getOperator( Node n ) { } d_par_op_map[op][tn1][tn2] = n; return n; - }else if( n.getKind()==APPLY_UF ){ + }else if( inst::Trigger::isAtomicTrigger( n ) ){ return n.getOperator(); }else{ return Node::null(); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9db32f894..57cf9001b 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -101,7 +101,12 @@ void TheoryUF::check(Effort level) { if (atom.getKind() == kind::EQUAL) { d_equalityEngine.assertEquality(atom, polarity, fact); } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) { - // do nothing + if( d_thss == NULL ){ + std::stringstream ss; + ss << "Cardinality constraint " << atom << " was asserted, but the logic does not allow it." << std::endl; + ss << "Try using a logic containing \"UFC\"." << std::endl; + throw Exception( ss.str() ); + } } else { d_equalityEngine.assertPredicate(atom, polarity, fact); } diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 8d70e4ffc..4d45d9148 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -36,6 +36,7 @@ namespace CVC4 { namespace expr { namespace attr { struct DatatypeIndexTag {}; + struct DatatypeConsIndexTag {}; struct DatatypeFiniteTag {}; struct DatatypeWellFoundedTag {}; struct DatatypeFiniteComputedTag {}; @@ -45,6 +46,7 @@ namespace expr { }/* CVC4::expr namespace */ typedef expr::Attribute DatatypeIndexAttr; +typedef expr::Attribute DatatypeConsIndexAttr; typedef expr::Attribute DatatypeFiniteAttr; typedef expr::Attribute DatatypeWellFoundedAttr; typedef expr::Attribute DatatypeFiniteComputedAttr; @@ -81,6 +83,20 @@ size_t Datatype::indexOf(Expr item) { } } +size_t Datatype::cindexOf(Expr item) { + ExprManagerScope ems(item); + CheckArgument(item.getType().isSelector(), + item, + "arg must be a datatype selector"); + TNode n = Node::fromExpr(item); + if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){ + return cindexOf( item[0] ); + }else{ + Assert(n.hasAttribute(DatatypeConsIndexAttr())); + return n.getAttribute(DatatypeConsIndexAttr()); + } +} + void Datatype::resolve(ExprManager* em, const std::map& resolutions, const std::vector& placeholders, @@ -103,7 +119,7 @@ void Datatype::resolve(ExprManager* em, d_resolved = true; size_t index = 0; for(std::vector::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) { - (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements); + (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements, index); Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index); Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); } @@ -401,7 +417,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, const std::vector& placeholders, const std::vector& replacements, const std::vector< SortConstructorType >& paramTypes, - const std::vector< DatatypeType >& paramReplacements) + const std::vector< DatatypeType >& paramReplacements, size_t cindex) throw(IllegalArgumentException, DatatypeResolutionException) { CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager"); @@ -447,6 +463,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, } (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr(); } + Node::fromExpr((*i).d_selector).setAttribute(DatatypeConsIndexAttr(), cindex); Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++); (*i).d_resolved = true; } diff --git a/src/util/datatype.h b/src/util/datatype.h index 99a303950..02e0b6be8 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -191,7 +191,7 @@ private: const std::vector& placeholders, const std::vector& replacements, const std::vector< SortConstructorType >& paramTypes, - const std::vector< DatatypeType >& paramReplacements) + const std::vector< DatatypeType >& paramReplacements, size_t cindex) throw(IllegalArgumentException, DatatypeResolutionException); friend class Datatype; @@ -434,6 +434,12 @@ public: */ static size_t indexOf(Expr item) CVC4_PUBLIC; + /** + * Get the index of constructor corresponding to selector. (Zero is + * always the first index.) + */ + static size_t cindexOf(Expr item) CVC4_PUBLIC; + /** The type for iterators over constructors. */ typedef DatatypeConstructorIterator iterator; /** The (const) type for iterators over constructors. */ diff --git a/test/regress/regress0/bug512.smt2 b/test/regress/regress0/bug512.smt2 index b0c970f37..1c8a0626a 100644 --- a/test/regress/regress0/bug512.smt2 +++ b/test/regress/regress0/bug512.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --tlimit-per 2500 -iq ; EXPECT: unknown -; EXPECT: (:reason-unknown timeout) +; EXPECT: (:reason-unknown incomplete) ; EXPECT: unsat (set-option :print-success false) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt index 536bc241f..f62f057e4 100644 --- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt +++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt @@ -1,4 +1,4 @@ -% COMMAND-LINE: --finite-model-find +% COMMAND-LINE: --finite-model-find --mbqi=gen-ev % EXPECT: unsat (benchmark Isabelle :status sat diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index b9a87231f..395054d67 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -23,18 +23,23 @@ TESTS = \ agree466.smt2 \ ALG008-1.smt2 \ german169.smt2 \ - Hoare-z3.931718.smt \ QEpres-uf.855035.smt \ agree467.smt2 \ Arrow_Order-smtlib.778341.smt \ german73.smt2 \ PUZ001+1.smt2 \ refcount24.cvc.smt2 \ - bug0909.smt2 \ - fmf-bound-int.smt2 + fmf-bound-int.smt2 \ + fc-simple.smt2 \ + fc-unsat-tot-2.smt2 \ + fc-unsat-pent.smt2 \ + fc-pigeonhole19.smt2 EXTRA_DIST = $(TESTS) +# disabled for now : +# Hoare-z3.931718.smt bug0909.smt2 + #if CVC4_BUILD_PROFILE_COMPETITION #else #TESTS += \ diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smt b/test/regress/regress0/fmf/QEpres-uf.855035.smt index 980e5fd49..2945c8f4d 100644 --- a/test/regress/regress0/fmf/QEpres-uf.855035.smt +++ b/test/regress/regress0/fmf/QEpres-uf.855035.smt @@ -1,4 +1,4 @@ -% COMMAND-LINE: --finite-model-find +% COMMAND-LINE: --finite-model-find --mbqi=gen-ev % EXPECT: sat (benchmark Isabelle :status sat diff --git a/test/regress/regress0/fmf/fc-pigeonhole19.smt2 b/test/regress/regress0/fmf/fc-pigeonhole19.smt2 new file mode 100755 index 000000000..15c36682c --- /dev/null +++ b/test/regress/regress0/fmf/fc-pigeonhole19.smt2 @@ -0,0 +1,20 @@ +(set-logic UFC) +(set-info :status unsat) + +(declare-sort P 0) +(declare-sort H 0) + +(declare-fun p () P) +(declare-fun h () H) + +; pigeonhole using native cardinality constraints +(assert (fmf.card p 19)) +(assert (not (fmf.card p 18))) +(assert (fmf.card h 18)) +(assert (not (fmf.card h 17))) + +; each pigeon has different holes +(declare-fun f (P) H) +(assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2)))))) + +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/fmf/fc-simple.smt2 b/test/regress/regress0/fmf/fc-simple.smt2 new file mode 100755 index 000000000..d1fd2301c --- /dev/null +++ b/test/regress/regress0/fmf/fc-simple.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_UFC) +(set-info :status unsat) + +(declare-sort U 0) + +(declare-fun a () U) +(declare-fun c () U) + +(assert (fmf.card c 2)) +(assert (not (fmf.card a 4))) + +(check-sat) diff --git a/test/regress/regress0/fmf/fc-unsat-pent.smt2 b/test/regress/regress0/fmf/fc-unsat-pent.smt2 new file mode 100755 index 000000000..f1721cb04 --- /dev/null +++ b/test/regress/regress0/fmf/fc-unsat-pent.smt2 @@ -0,0 +1,20 @@ +(set-logic QF_UFC) +(set-info :status unsat) + +(declare-sort U 0) + +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) +(declare-fun d () U) +(declare-fun e () U) + +(assert (not (= a b))) +(assert (not (= b c))) +(assert (not (= c d))) +(assert (not (= d e))) +(assert (not (= e a))) + +(assert (fmf.card c 2)) + +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 new file mode 100755 index 000000000..d946974ed --- /dev/null +++ b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 @@ -0,0 +1,14 @@ +(set-logic UFC) +(set-info :status unsat) + +(declare-sort U 0) + +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) + +(assert (not (fmf.card a 2))) + +(assert (forall ((x U)) (or (= x a) (= x b)))) + +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/quantifiers/bug269.smt2 b/test/regress/regress0/quantifiers/bug269.smt2 index 0d5aedbb3..2e50030d1 100644 --- a/test/regress/regress0/quantifiers/bug269.smt2 +++ b/test/regress/regress0/quantifiers/bug269.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat (set-logic LRA) (set-info :status unsat) (declare-fun x4 () Real) diff --git a/test/regress/regress0/quantifiers/burns13.smt2 b/test/regress/regress0/quantifiers/burns13.smt2 index ad970a2b2..3424c161e 100644 --- a/test/regress/regress0/quantifiers/burns13.smt2 +++ b/test/regress/regress0/quantifiers/burns13.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant --decision=internal +; EXPECT: unsat (set-logic AUFLIA) (set-info :source | Burns mutual exclusion protocol. This is a benchmark of the haRVey theorem prover. It was translated to SMT-LIB by Leonardo de Moura |) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index 3a3a097bd..31f99905c 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -23,16 +23,16 @@ MAKEFLAGS = -k # put it below in "TESTS +=" TESTS = \ length_trick.smt2 \ - length_trick2.smt2 \ length_gen_020.smt2 \ datatypes.smt2 \ datatypes_sat.smt2 \ reachability_back_to_the_future.smt2 \ relation.smt2 \ simulate_rewriting.smt2 \ - native_arrays.smt2 + native_arrays.smt2 \ + read5.smt2 -# reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2 +# length_trick2.smt2 reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/rewriterules/read5.smt2 b/test/regress/regress0/rewriterules/read5.smt2 new file mode 100755 index 000000000..e66df7c7e --- /dev/null +++ b/test/regress/regress0/rewriterules/read5.smt2 @@ -0,0 +1,35 @@ +(set-logic AUF) +(set-info :source | +Translated from old SVC processor verification benchmarks. Contact Clark +Barrett at barrett@cs.nyu.edu for more information. + +This benchmark was automatically translated into SMT-LIB format from +CVC format using CVC Lite +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0)(declare-sort Arr 0)(declare-fun aselect (Arr Index) Element)(declare-fun astore (Arr Index Element) Arr)(declare-fun k (Arr Arr) Index) +(declare-fun a () Index) +(declare-fun aaa () Index) +(declare-fun aa () Index) +(declare-fun S () Arr) +(declare-fun vvv () Element) +(declare-fun v () Element) +(declare-fun vv () Element) +(declare-fun bbb () Index) +(declare-fun www () Element) +(declare-fun bb () Index) +(declare-fun ww () Element) +(declare-fun b () Index) +(declare-fun w () Element) +(declare-fun SS () Arr) +(assert (let ((?v_3 (ite (= a aa) false true)) (?v_4 (ite (= aa aaa) false true)) (?v_1 (astore (astore (astore S a v) aa vv) aaa vvv)) (?v_0 (astore S aaa vvv)) (?v_2 (astore S aa vv))) (not (ite (ite (ite (ite (= a aaa) false true) (ite ?v_3 ?v_4 false) false) (ite (= (astore (astore ?v_0 a v) aa vv) ?v_1) (ite (= (astore (astore ?v_0 aa vv) a v) ?v_1) (ite (= (astore (astore ?v_2 a v) aaa vvv) ?v_1) (= (astore (astore ?v_2 aaa vvv) a v) ?v_1) false) false) false) true) (ite (ite (= ?v_1 (astore (astore (astore S bbb www) bb ww) b w)) (ite (ite ?v_3 (ite ?v_4 (ite (ite (= aa b) false true) (ite (ite (= aa bb) false true) (ite (= aa bbb) false true) false) false) false) false) (= (aselect S aa) vv) true) true) (ite (= S (astore SS a v)) (= S (astore SS a (aselect S a))) true) false) false)))) +; rewrite rule definition of arrays theory +(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (=> (not (= ?i ?j)) (= (aselect (astore ?x ?i ?e) ?j) (aselect ?x ?j))) :rewrite-rule))) +(assert (forall ((?x Arr) (?i Index) (?e Element)) (! (=> true (= (aselect (astore ?x ?i ?e) ?i) ?e)) :rewrite-rule))) +(assert (forall ((?x Arr) (?y Arr)) (! (=> (not (= ?x ?y)) (not (= (aselect ?x (k ?x ?y)) (aselect ?y (k ?x ?y))))) :rewrite-rule))) +(assert (forall ((?x Arr) (?y Arr)) (! (! (=> true (or (= ?x ?y) (not (= ?x ?y)))) :pattern (?x)) :rewrite-rule))) +(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (! (=> true (or (= ?i ?j) (not (= ?i ?j)))) :pattern ((aselect (astore ?x ?i ?e) ?j))) :rewrite-rule)))(check-sat) +(exit) diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am index e0c8a2b48..e9274d2ee 100644 --- a/test/regress/regress0/tptp/Makefile.am +++ b/test/regress/regress0/tptp/Makefile.am @@ -35,7 +35,6 @@ TESTS = \ tff0.p \ tff0-arith.p \ ARI086$(equals)1.p \ - BOO003-4.p \ DAT001$(equals)1.p \ KRS018+1.p \ KRS063+1.p \ @@ -62,6 +61,7 @@ TEST_DEPS_DIST = \ EXTRA_DIST = $(TESTS) \ $(TEST_DEPS_DIST) \ BOO027-1.p \ + BOO003-4.p \ MGT031-1.p \ NLP114-1.p \ SYN075+1.p -- cgit v1.2.3 From 15f00378d60ec263e12b36d8f4e2ce4a417e8627 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Thu, 10 Apr 2014 12:56:53 -0500 Subject: minor fix for strings --- src/theory/strings/regexp_operation.cpp | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index d719b4e1a..0dd43b229 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -41,10 +41,6 @@ RegExpOpr::RegExpOpr() { d_emptySingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString ); std::vector< Node > nvec; d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ); - // All Charactors = all printable ones 32-126 - //d_char_start = 'a';//' '; - //d_char_end = 'c';//'~'; - //d_sigma = mkAllExceptOne( '\0' ); d_sigma = NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA, nvec ); d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma ); d_card = 256; @@ -896,15 +892,13 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes } case kind::REGEXP_CONCAT: { //TODO: rewrite empty + Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s); Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero), NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s), b1 ) ); - Node s1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType()); - Node s2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType()); - Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, s1, s2); - Node s12 = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2)); - Node s1len = b1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1)); + Node s1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, d_zero, b1)); + Node s2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1))); Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate(); if(r[0].getKind() == kind::STRING_TO_REGEXP) { s1r1 = s1.eqNode(r[0][0]).negate(); @@ -928,8 +922,6 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes } conc = NodeManager::currentNM()->mkNode(kind::OR, s1r1, s2r2); - conc = NodeManager::currentNM()->mkNode(kind::AND, s12, s1len, conc); - conc = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, conc); conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc); conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc); break; -- cgit v1.2.3 From eed206f398801a6ff5b3d6051702c444911c575d Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Thu, 10 Apr 2014 12:56:53 -0500 Subject: minor fix for strings --- src/theory/strings/regexp_operation.cpp | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index d719b4e1a..0dd43b229 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -41,10 +41,6 @@ RegExpOpr::RegExpOpr() { d_emptySingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString ); std::vector< Node > nvec; d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ); - // All Charactors = all printable ones 32-126 - //d_char_start = 'a';//' '; - //d_char_end = 'c';//'~'; - //d_sigma = mkAllExceptOne( '\0' ); d_sigma = NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA, nvec ); d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma ); d_card = 256; @@ -896,15 +892,13 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes } case kind::REGEXP_CONCAT: { //TODO: rewrite empty + Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s); Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero), NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s), b1 ) ); - Node s1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType()); - Node s2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType()); - Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, s1, s2); - Node s12 = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2)); - Node s1len = b1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1)); + Node s1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, d_zero, b1)); + Node s2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1))); Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate(); if(r[0].getKind() == kind::STRING_TO_REGEXP) { s1r1 = s1.eqNode(r[0][0]).negate(); @@ -928,8 +922,6 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes } conc = NodeManager::currentNM()->mkNode(kind::OR, s1r1, s2r2); - conc = NodeManager::currentNM()->mkNode(kind::AND, s12, s1len, conc); - conc = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, conc); conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc); conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc); break; -- cgit v1.2.3 From 65128efc1d0a4c2007ebb7b47712888481c07843 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 10 Apr 2014 16:38:37 -0400 Subject: Boolean terms conversion fix for datatypes, fixes a problem Andy discovered on his branch. --- src/smt/boolean_terms.cpp | 23 ++++++++++++++++++++--- src/smt/boolean_terms.h | 2 ++ 2 files changed, 22 insertions(+), 3 deletions(-) diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 4555aac51..111324dfa 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -46,7 +46,8 @@ BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) : d_varCache(smt.d_userContext), d_termCache(smt.d_userContext), d_typeCache(), - d_datatypeCache() { + d_datatypeCache(), + d_datatypeReverseCache() { // set up our "false" and "true" conversions based on command-line option if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS || @@ -116,6 +117,10 @@ static inline bool isBoolean(TNode top, unsigned i) { // to be for model-substitution, so the "in" is a Boolean-term-converted // node, and "as" is the original. See how it's used in function // handling, below. +// +// Note this isn't the case any longer, and parts of what's below have +// been repurposed for *forward* conversion, meaning this works in either +// direction. Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { if(in.getType() == as) { return in; @@ -133,7 +138,12 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { } Assert(as.isDatatype()); const Datatype* dt2 = &as.getDatatype(); - const Datatype* dt1 = d_datatypeCache[dt2]; + const Datatype* dt1; + if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { + dt1 = d_datatypeCache[dt2]; + } else { + dt1 = d_datatypeReverseCache[dt2]; + } Assert(dt1 != NULL, "expected datatype in cache"); Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes"); Node out; @@ -165,7 +175,12 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { fromParams.push_back(TypeNode::fromType(dt2->getParameter(i))); toParams.push_back(as[i + 1]); } - const Datatype* dt1 = d_datatypeCache[dt2]; + const Datatype* dt1; + if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { + dt1 = d_datatypeCache[dt2]; + } else { + dt1 = d_datatypeReverseCache[dt2]; + } Assert(dt1 != NULL, "expected datatype in cache"); Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes"); Node out; @@ -259,11 +274,13 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw( } } out = &newD; + d_datatypeReverseCache[&newD] = &dt; return newD; } } } + // this is identity; don't need the reverse cache out = &dt; return dt; diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index b289e3469..bdd9ff839 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -69,6 +69,8 @@ class BooleanTermConverter { BooleanTermTypeCache d_typeCache; /** The cache used during Boolean term datatype conversion */ BooleanTermDatatypeCache d_datatypeCache; + /** A (reverse) cache for Boolean term datatype conversion */ + BooleanTermDatatypeCache d_datatypeReverseCache; Node rewriteAs(TNode in, TypeNode as) throw(); -- cgit v1.2.3 From 6ae07a91cdd4f20f8fdccd7e31d217c6ca34ee45 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Apr 2014 15:50:56 -0500 Subject: Expand definitions in theory datatypes, now has the expected semantics for incorrectly applied selector terms. --- src/parser/smt2/smt2.cpp | 1 + src/printer/cvc/cvc_printer.cpp | 1 + src/printer/smt2/smt2_printer.cpp | 1 + src/smt/boolean_terms.cpp | 4 +- src/theory/datatypes/datatypes_rewriter.h | 4 +- src/theory/datatypes/kinds | 2 + src/theory/datatypes/theory_datatypes.cpp | 55 +++++++++++++++++++--- src/theory/datatypes/theory_datatypes.h | 3 ++ src/theory/datatypes/theory_datatypes_type_rules.h | 2 +- src/theory/quantifiers/options_handlers.h | 23 ++++----- src/theory/quantifiers/quant_conflict_find.cpp | 2 +- src/theory/quantifiers/trigger.cpp | 2 +- src/theory/theory_model.cpp | 4 +- test/regress/regress0/datatypes/Makefile.am | 3 +- test/regress/regress0/datatypes/datatype1.cvc | 2 +- test/regress/regress0/datatypes/datatype3.cvc | 2 +- test/regress/regress0/datatypes/wrong-sel-simp.cvc | 2 +- 17 files changed, 80 insertions(+), 33 deletions(-) diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 64b321613..e9e6ba857 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -158,6 +158,7 @@ void Smt2::addTheory(Theory theory) { Parser::addOperator(kind::APPLY_CONSTRUCTOR); Parser::addOperator(kind::APPLY_TESTER); Parser::addOperator(kind::APPLY_SELECTOR); + Parser::addOperator(kind::APPLY_SELECTOR_TOTAL); break; case THEORY_STRINGS: diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 4d784c383..63529c2a5 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -316,6 +316,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; case kind::APPLY_CONSTRUCTOR: case kind::APPLY_SELECTOR: + case kind::APPLY_SELECTOR_TOTAL: case kind::APPLY_TESTER: toStream(op, n.getOperator(), depth, types, false); break; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ea335f2e5..1250bc659 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -424,6 +424,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::APPLY_TESTER: case kind::APPLY_CONSTRUCTOR: case kind::APPLY_SELECTOR: + case kind::APPLY_SELECTOR_TOTAL: case kind::PARAMETRIC_DATATYPE: break; diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 111324dfa..e46a76ed7 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -152,7 +152,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); appctorb << (*dt2)[i].getConstructor(); for(size_t j = 0; j < ctor.getNumArgs(); ++j) { - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType())); + appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType())); } Node appctor = appctorb; if(i == 0) { @@ -191,7 +191,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { for(size_t j = 0; j < ctor.getNumArgs(); ++j) { TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()); asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end()); - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), asType); + appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType); } Node appctor = appctorb; if(i == 0) { diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 37a656555..8cb3fb4a2 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -88,7 +88,7 @@ public: const Record& rec = in[0].getType().getAttribute(expr::DatatypeRecordAttr()).getConst(); return RewriteResponse(REWRITE_DONE, in[0][rec.getIndex(in.getOperator().getConst().getField())]); } - if(in.getKind() == kind::APPLY_SELECTOR && + if(in.getKind() == kind::APPLY_SELECTOR_TOTAL && (in[0].getKind() == kind::TUPLE || in[0].getKind() == kind::RECORD)) { // These strange (half-tuple-converted) terms can be created by // the system if you have something like "foo.1" for a tuple @@ -118,7 +118,7 @@ public: Debug("tuprec") << "==> returning " << in[0][selectorIndex] << std::endl; return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); } - if(in.getKind() == kind::APPLY_SELECTOR && + if(in.getKind() == kind::APPLY_SELECTOR_TOTAL && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { // Have to be careful not to rewrite well-typed expressions // where the selector doesn't match the constructor, diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index bb6fd4373..b222738ae 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -39,6 +39,7 @@ cardinality TESTER_TYPE \ parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application" parameterized APPLY_SELECTOR SELECTOR_TYPE 1: "selector application" +parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1: "selector application (total)" parameterized APPLY_TESTER TESTER_TYPE 1: "tester application" @@ -82,6 +83,7 @@ constant ASCRIPTION_TYPE \ typerule APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule typerule APPLY_SELECTOR ::CVC4::theory::datatypes::DatatypeSelectorTypeRule +typerule APPLY_SELECTOR_TOTAL ::CVC4::theory::datatypes::DatatypeSelectorTypeRule typerule APPLY_TESTER ::CVC4::theory::datatypes::DatatypeTesterTypeRule typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionTypeRule diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index b00b4148d..0b0f5807c 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -54,7 +54,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); - d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR); + d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); } @@ -318,6 +318,47 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { flushPendingFacts(); } +Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { + switch( n.getKind() ){ + case kind::APPLY_SELECTOR: { + Node selector = n.getOperator(); + Expr selectorExpr = selector.toExpr(); + size_t selectorIndex = Datatype::cindexOf(selectorExpr); + const Datatype& dt = Datatype::datatypeOf(selectorExpr); + const DatatypeConstructor& c = dt[selectorIndex]; + Expr tester = c.getTester(); + Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] ); + tst = Rewriter::rewrite( tst ); + Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] ); + Node n_ret; + if( tst==NodeManager::currentNM()->mkConst( true ) ){ + n_ret = sel; + }else{ + if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){ + std::stringstream ss; + ss << selector << "_uf"; + d_exp_def_skolem[ selector ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(), + NodeManager::currentNM()->mkFunctionType( n[0].getType(), n.getType() ) ); + } + Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0] ); + if( tst==NodeManager::currentNM()->mkConst( false ) ){ + n_ret = sk; + }else{ + n_ret = NodeManager::currentNM()->mkNode( kind::ITE, tst, sel, sk ); + } + } + //n_ret = Rewriter::rewrite( n_ret ); + Trace("dt-expand") << "Expand def : " << n << " to " << n_ret << std::endl; + return n_ret; + } + break; + default: + return n; + break; + } + Unreachable(); +} + void TheoryDatatypes::presolve() { Debug("datatypes") << "TheoryDatatypes::presolve()" << endl; } @@ -332,7 +373,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { } TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst().getIndex()].getSelector()), in[0]); + return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst().getIndex()].getSelector()), in[0]); } else if(in.getKind() == kind::RECORD_SELECT) { TypeNode t = in[0].getType(); if(t.hasAttribute(expr::DatatypeRecordAttr())) { @@ -340,7 +381,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { } TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst().getField()].getSelector()), in[0]); + return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst().getField()].getSelector()), in[0]); } TypeNode t = in.getType(); @@ -404,7 +445,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { b << in[1]; Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl; } else { - b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][i].getSelector()), in[0]); + b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][i].getSelector()), in[0]); Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl; } } @@ -848,7 +889,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ } void TheoryDatatypes::collapseSelector( Node s, Node c ) { - Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, s.getOperator(), c ); + Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c ); Node rr = Rewriter::rewrite( r ); //if( r!=rr ){ //Node eq_exp = NodeManager::currentNM()->mkConst(true); @@ -1075,7 +1116,7 @@ void TheoryDatatypes::collectTerms( Node n ) { //eqc->d_selectors = true; } */ - }else if( n.getKind() == APPLY_SELECTOR ){ + }else if( n.getKind() == APPLY_SELECTOR_TOTAL ){ //we must also record which selectors exist Debug("datatypes") << " Found selector " << n << endl; if (n.getType().isBoolean()) { @@ -1117,7 +1158,7 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, std::vector< Node > children; children.push_back( Node::fromExpr( dt[index].getConstructor() ) ); for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){ - Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[index][i].getSelector() ), n ); + Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), n ); if( mkVar ){ TypeNode tn = nc.getType(); if( dt.isParametric() ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 3a29433f8..2a93878d0 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -166,6 +166,8 @@ private: std::vector< Node > d_pending; std::map< Node, Node > d_pending_exp; std::vector< Node > d_pending_merge; + /** expand definition skolem functions */ + std::map< Node, Node > d_exp_def_skolem; private: /** assert fact */ void assertFact( Node fact, Node exp ); @@ -208,6 +210,7 @@ public: void check(Effort e); void preRegisterTerm(TNode n); + Node expandDefinition(LogicRequest &logicRequest, Node n); Node ppRewrite(TNode n); void presolve(); void addSharedTerm(TNode t); diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 527d110e0..d08b511dd 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -98,7 +98,7 @@ struct DatatypeConstructorTypeRule { struct DatatypeSelectorTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw(TypeCheckingExceptionPrivate) { - Assert(n.getKind() == kind::APPLY_SELECTOR); + Assert(n.getKind() == kind::APPLY_SELECTOR || n.getKind() == kind::APPLY_SELECTOR_TOTAL ); TypeNode selType = n.getOperator().getType(check); Type t = selType[0].toType(); Assert( t.isDatatype() ); diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 164e9e643..b7e624a66 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -92,8 +92,8 @@ instgen \n\ + Use instantiation algorithm that mimics Inst-Gen calculus. \n\ \n\ gen-ev \n\ -+ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\ - model finding paper.\n\ ++ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ + model finding paper based on generalizing evaluations.\n\ \n\ fmc-interval \n\ + Same as default, but with intervals for models of integer functions.\n\ @@ -131,9 +131,6 @@ conflict \n\ partial \n\ + Apply QCF algorithm to instantiate heuristically as well. \n\ \n\ -partial \n\ -+ Apply QCF to instantiate heuristically as well. \n\ -\n\ mc \n\ + Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\ \n\ @@ -217,21 +214,21 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar } inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "gen-ev") { + if(optarg == "gen-ev") { return MBQI_GEN_EVAL; - } else if(optarg == "none") { + } else if(optarg == "none") { return MBQI_NONE; - } else if(optarg == "instgen") { + } else if(optarg == "instgen") { return MBQI_INST_GEN; - } else if(optarg == "default" || optarg == "fmc") { + } else if(optarg == "default" || optarg == "fmc") { return MBQI_FMC; - } else if(optarg == "fmc-interval") { + } else if(optarg == "fmc-interval") { return MBQI_FMC_INTERVAL; - } else if(optarg == "interval") { + } else if(optarg == "interval") { return MBQI_INTERVAL; - } else if(optarg == "trust") { + } else if(optarg == "trust") { return MBQI_TRUST; - } else if(optarg == "help") { + } else if(optarg == "help") { puts(mbqiModeHelp.c_str()); exit(1); } else { diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index c0b318f23..e27d438be 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1488,7 +1488,7 @@ bool MatchGen::isHandledBoolConnective( TNode n ) { bool MatchGen::isHandledUfTerm( TNode n ) { return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT || - n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;// || n.getKind()==GEQ; + n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; } Node MatchGen::getOperator( QuantConflictFind * p, Node n ) { diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 6912c9e89..3de12b9c9 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -324,7 +324,7 @@ bool Trigger::isUsableTrigger( Node n, Node f ){ bool Trigger::isAtomicTrigger( Node n ){ return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE || - n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER; + n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; } bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 405fceb6f..f207bdb8e 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -41,7 +41,7 @@ TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFunc d_equalityEngine->addFunctionKind(kind::SELECT); // d_equalityEngine->addFunctionKind(kind::STORE); d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR); - d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR); + d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine->addFunctionKind(kind::APPLY_TESTER); d_eeContext->push(); } @@ -422,7 +422,7 @@ TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( t bool TheoryEngineModelBuilder::isAssignable(TNode n) { - return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR); + return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL); } diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 84adb4f84..e8a8f16f5 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -31,7 +31,6 @@ TESTS = \ datatype0.cvc \ datatype1.cvc \ datatype2.cvc \ - datatype3.cvc \ datatype4.cvc \ datatype13.cvc \ empty_tuprec.cvc \ @@ -64,6 +63,8 @@ TESTS = \ FAILING_TESTS = \ datatype-dump.cvc +# takes a long time to build model on debug : datatype3.cvc + EXTRA_DIST = $(TESTS) if CVC4_BUILD_PROFILE_COMPETITION diff --git a/test/regress/regress0/datatypes/datatype1.cvc b/test/regress/regress0/datatypes/datatype1.cvc index 5172eeb48..3934959f1 100644 --- a/test/regress/regress0/datatypes/datatype1.cvc +++ b/test/regress/regress0/datatypes/datatype1.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: invalid DATATYPE tree = node(left : tree, right : tree) | leaf diff --git a/test/regress/regress0/datatypes/datatype3.cvc b/test/regress/regress0/datatypes/datatype3.cvc index 5f130b6ae..fff1a5dd7 100644 --- a/test/regress/regress0/datatypes/datatype3.cvc +++ b/test/regress/regress0/datatypes/datatype3.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: invalid DATATYPE tree = node(left : tree, right : tree) | leaf diff --git a/test/regress/regress0/datatypes/wrong-sel-simp.cvc b/test/regress/regress0/datatypes/wrong-sel-simp.cvc index 7455f809c..b0dbdc46e 100644 --- a/test/regress/regress0/datatypes/wrong-sel-simp.cvc +++ b/test/regress/regress0/datatypes/wrong-sel-simp.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: invalid DATATYPE nat = succ(pred : nat) | zero END; -- cgit v1.2.3 From 9042fc86692b6dc67ed5ba6bd721752d9a5c5389 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 10 Apr 2014 18:34:44 -0400 Subject: Fix the build; --check-proof works for UF but not for the new UFC logic. --- src/smt/smt_engine_check_proof.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index a731ff024..4c218b48c 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -57,10 +57,11 @@ void SmtEngine::checkProof() { Chat() << "checking proof..." << endl; - if(!d_logic.isPure(theory::THEORY_BOOL) && - !d_logic.isPure(theory::THEORY_UF)) { + if( ! ( d_logic.isPure(theory::THEORY_BOOL) || + ( d_logic.isPure(theory::THEORY_UF) && + ! d_logic.hasCardinalityConstraints() ) ) ) { // no checking for these yet - Notice() << "Notice: no proof-checking for non-UF proofs yet" << endl; + Notice() << "Notice: no proof-checking for non-UF/Bool proofs yet" << endl; return; } -- cgit v1.2.3 From 48653e7a5104479b91523afa449810a9cc2fd160 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 10 Apr 2014 20:06:31 -0400 Subject: setType -> setOfType, resolves bug 556 --- src/cvc4.i | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cvc4.i b/src/cvc4.i index c0042b513..fcd5a8470 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -71,7 +71,7 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; %template(vectorString) std::vector< std::string >; %template(vectorPairStringType) std::vector< std::pair< std::string, CVC4::Type > >; %template(pairStringType) std::pair< std::string, CVC4::Type >; -%template(setType) std::set< CVC4::Type >; +%template(setOfType) std::set< CVC4::Type >; %template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >; // This is unfortunate, but seems to be necessary; if we leave NULL -- cgit v1.2.3 From d8e31379256a8fc0c6d7993e42fc94a9dc35f4ce Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 11 Apr 2014 15:30:31 -0400 Subject: Better support for building with mingw64; thanks to Nicolas Roche @ Altran for the fix. --- src/lib/clock_gettime.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h index 43c3395a4..8860e717b 100644 --- a/src/lib/clock_gettime.h +++ b/src/lib/clock_gettime.h @@ -30,7 +30,7 @@ /* otherwise, we have to define it */ -#if defined(__WIN32__) && !defined(__WIN64__) +#if defined(__WIN32__) && !defined(_W64) #ifdef __cplusplus extern "C" { @@ -45,12 +45,12 @@ struct timespec { }/* extern "C" */ #endif /* __cplusplus */ -#else /* !__WIN32__ || __WIN64__ */ +#else /* !__WIN32__ || _W64 */ /* get timespec from */ #include -#endif /* __WIN32__ && !__WIN64__ */ +#endif /* __WIN32__ && !_W64 */ #ifdef __cplusplus extern "C" { -- cgit v1.2.3 From b71bbbbc607b5ca0c2bec8b8cf6c7af596d21997 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Apr 2014 04:28:44 -0500 Subject: Add initial support for co-datatypes. --- src/compat/cvc3_compat.cpp | 2 +- src/parser/cvc/Cvc.g | 2 +- src/parser/smt2/Smt2.g | 38 ++-- src/smt/boolean_terms.cpp | 4 +- src/theory/builtin/kinds | 2 + src/theory/builtin/theory_builtin_type_rules.h | 18 ++ src/theory/datatypes/theory_datatypes.cpp | 284 +++++++++++++++++++++---- src/theory/datatypes/theory_datatypes.h | 8 + src/util/datatype.h | 18 +- 9 files changed, 310 insertions(+), 66 deletions(-) diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 27d1249a1..427282490 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1189,7 +1189,7 @@ void ValidityChecker::dataType(const std::vector& names, // Set up the datatype specifications. for(unsigned i = 0; i < names.size(); ++i) { - CVC4::Datatype dt(names[i]); + CVC4::Datatype dt(names[i], false); CVC4::CheckArgument(constructors[i].size() == selectors[i].size(), "expected sub-vectors in constructors and selectors vectors to match in size"); CVC4::CheckArgument(constructors[i].size() == types[i].size(), "expected sub-vectors in constructors and types vectors to match in size"); for(unsigned j = 0; j < constructors[i].size(); ++j) { diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 792c3cf9d..f9055f5db 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2018,7 +2018,7 @@ datatypeDef[std::vector& datatypes] params.push_back( t ); } )* RBRACKET )? - { datatypes.push_back(Datatype(id, params)); + { datatypes.push_back(Datatype(id, params, false)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 659fc97d9..2118a240d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -464,17 +464,8 @@ extendedCommand[CVC4::Command*& cmd] } /* Extended SMT-LIB set of commands syntax, not permitted in * --smtlib2 compliance mode. */ - : DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { /* open a scope to keep the UnresolvedTypes contained */ - PARSER_STATE->pushScope(true); } - LPAREN_TOK /* parametric sorts */ - ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { - sorts.push_back( PARSER_STATE->mkSort(name) ); } - )* - RPAREN_TOK - LPAREN_TOK ( LPAREN_TOK datatypeDef[dts, sorts] RPAREN_TOK )+ RPAREN_TOK - { PARSER_STATE->popScope(); - cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + : DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] + | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] | /* get model */ GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd = new GetModelCommand(); } @@ -603,6 +594,26 @@ extendedCommand[CVC4::Command*& cmd] { cmd = new SimplifyCommand(e); } ; + +datatypesDefCommand[bool isCo, CVC4::Command*& cmd] +@declarations { + std::vector dts; + std::string name; + std::vector sorts; +} + : { PARSER_STATE->checkThatLogicIsSet(); + /* open a scope to keep the UnresolvedTypes contained */ + PARSER_STATE->pushScope(true); } + LPAREN_TOK /* parametric sorts */ + ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { + sorts.push_back( PARSER_STATE->mkSort(name) ); } + )* + RPAREN_TOK + LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK + { PARSER_STATE->popScope(); + cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + ; + rewriterulesCommand[CVC4::Command*& cmd] @declarations { std::vector > sortedVarNames; @@ -1530,7 +1541,7 @@ nonemptyNumeralList[std::vector& numerals] /** * Parses a datatype definition */ -datatypeDef[std::vector& datatypes, std::vector< CVC4::Type >& params] +datatypeDef[bool isCo, std::vector& datatypes, std::vector< CVC4::Type >& params] @init { std::string id; } @@ -1548,7 +1559,7 @@ datatypeDef[std::vector& datatypes, std::vector< CVC4::Type >& p params.push_back( t ); } )* ']' )?*/ //AJR: this isn't necessary if we use z3's style - { datatypes.push_back(Datatype(id,params)); + { datatypes.push_back(Datatype(id,params,isCo)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); @@ -1623,6 +1634,7 @@ AS_TOK : 'as'; // extended commands DECLARE_DATATYPES_TOK : 'declare-datatypes'; +DECLARE_CODATATYPES_TOK : 'declare-codatatypes'; GET_MODEL_TOK : 'get-model'; ECHO_TOK : 'echo'; REWRITE_RULE_TOK : 'assert-rewrite'; diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index e46a76ed7..c779af4ff 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -228,9 +228,9 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw( } vector newDtVector; if(dt.isParametric()) { - newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters())); + newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters(), false)); } else { - newDtVector.push_back(Datatype(dt.getName() + "'")); + newDtVector.push_back(Datatype(dt.getName() + "'", false)); } Datatype& newDt = newDtVector.front(); Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl; diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index b3383e6c4..d140d1990 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -302,6 +302,7 @@ variable SKOLEM "skolem var" operator SEXPR 0: "a symbolic expression" operator LAMBDA 2 "lambda" +operator MU 2 "mu" parameterized CHAIN CHAIN_OP 2: "chained operator" constant CHAIN_OP \ @@ -334,6 +335,7 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule +typerule MU ::CVC4::theory::builtin::MuTypeRule typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index c7143bdeb..f35286f05 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -164,6 +164,24 @@ public: } };/* class LambdaTypeRule */ +class MuTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + if( n[0].getType(check) != nodeManager->boundVarListType() ) { + std::stringstream ss; + ss << "expected a bound var list for MU expression, got `" + << n[0].getType().toString() << "'"; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + std::vector argTypes; + for(TNode::iterator i = n[0].begin(); i != n[0].end(); ++i) { + argTypes.push_back((*i).getType()); + } + TypeNode rangeType = n[1].getType(check); + return nodeManager->mkFunctionType(argTypes, rangeType); + } +};/* class MuTypeRule */ + class ChainTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 0b0f5807c..fc37c5417 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -123,13 +123,19 @@ void TheoryDatatypes::check(Effort e) { if( e == EFFORT_FULL ) { //check for cycles - checkCycles(); - if( d_conflict ){ - return; - } + bool addedFact; + do { + checkCycles(); + addedFact = !d_pending.empty() || !d_pending_merge.empty(); + flushPendingFacts(); + if( d_conflict ){ + return; + } + }while( addedFact ); + //check for splits Debug("datatypes-split") << "Check for splits " << e << endl; - bool addedFact = false; + addedFact = false; do { eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ @@ -146,7 +152,7 @@ void TheoryDatatypes::check(Effort e) { Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n ); d_pending.push_back( t ); d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true ); - Trace("datatypes-infer") << "DtInfer : " << t << ", trivial" << std::endl; + Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl; d_infer.push_back( t ); }else{ std::vector< bool > pcons; @@ -493,21 +499,37 @@ bool TheoryDatatypes::propagate(TNode literal){ return ok; } +void TheoryDatatypes::addAssumptions( std::vector& assumptions, std::vector& tassumptions ) { + for( unsigned i=0; i& assumptions ) { + if( a!=b ){ + std::vector tassumptions; + d_equalityEngine.explainEquality(a, b, polarity, tassumptions); + addAssumptions( assumptions, tassumptions ); + } +} + +void TheoryDatatypes::explainPredicate( TNode p, bool polarity, std::vector& assumptions ) { + std::vector tassumptions; + d_equalityEngine.explainPredicate(p, polarity, tassumptions); + addAssumptions( assumptions, tassumptions ); +} + /** explain */ void TheoryDatatypes::explain(TNode literal, std::vector& assumptions){ Debug("datatypes-explain") << "Explain " << literal << std::endl; bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - std::vector tassumptions; if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions); + explainEquality( atom[0], atom[1], polarity, assumptions ); } else { - d_equalityEngine.explainPredicate(atom, polarity, tassumptions); - } - for( unsigned i=0; i assumptions; explain( t, assumptions ); - explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions ); + explainEquality( eqc->d_constructor.get(), tt[0], true, assumptions ); d_conflictNode = mkAnd( assumptions ); Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); @@ -808,7 +830,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; d_pending.push_back( t_concl ); d_pending_exp[ t_concl ] = t_concl_exp; - Trace("datatypes-infer") << "DtInfer : " << t_concl << " by " << t_concl_exp << std::endl; + Trace("datatypes-infer") << "DtInfer : label : " << t_concl << " by " << t_concl_exp << std::endl; d_infer.push_back( t_concl ); d_infer_exp.push_back( t_concl_exp ); return; @@ -822,7 +844,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ std::vector< TNode > assumptions; explain( j, assumptions ); explain( t, assumptions ); - explain( jt[0].eqNode( tt[0] ), assumptions ); + explainEquality( jt[0], tt[0], true, assumptions ); d_conflictNode = mkAnd( assumptions ); Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); @@ -866,7 +888,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ Node n = *i; std::vector< TNode > assumptions; explain( *i, assumptions ); - explain( c.eqNode( (*i)[0][0] ), assumptions ); + explainEquality( c, (*i)[0][0], true, assumptions ); d_conflictNode = mkAnd( assumptions ); Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); @@ -901,7 +923,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { d_pending.push_back( eq ); d_pending_exp[ eq ] = eq_exp; - Trace("datatypes-infer") << "DtInfer : " << eq << " by " << eq_exp << " (collapse selector)" << std::endl; + Trace("datatypes-infer") << "DtInfer : collapse sel : " << eq << " by " << eq_exp << std::endl; d_infer.push_back( eq ); d_infer_exp.push_back( eq_exp ); } @@ -1141,7 +1163,7 @@ void TheoryDatatypes::processNewTerm( Node n ){ Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n ); d_pending.push_back( eq ); d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true ); - Trace("datatypes-infer") << "DtInfer : " << eq << ", trivial" << std::endl; + Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl; d_infer.push_back( eq ); } } @@ -1219,7 +1241,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl; d_pending.push_back( eq ); d_pending_exp[ eq ] = exp; - Trace("datatypes-infer") << "DtInfer : " << eq << " by " << exp << std::endl; + Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp << std::endl; //eqc->d_inst.set( eq ); d_infer.push_back( eq ); d_infer_exp.push_back( exp ); @@ -1233,33 +1255,201 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ void TheoryDatatypes::checkCycles() { Debug("datatypes-cycle-check") << "Check cycles" << std::endl; + std::vector< Node > cod_eqc; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); if( DatatypesRewriter::isTermDatatype( eqc ) ) { - map< Node, bool > visited; - std::vector< TNode > expl; - Node cn = searchForCycle( eqc, eqc, visited, expl ); - //if we discovered a different cycle while searching this one - if( !cn.isNull() && cn!=eqc ){ - visited.clear(); - expl.clear(); - Node prev = cn; - cn = searchForCycle( cn, cn, visited, expl ); - Assert( prev==cn ); - } + const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); + if( !dt.isCodatatype() ){ + //do cycle checks + map< Node, bool > visited; + std::vector< TNode > expl; + Node cn = searchForCycle( eqc, eqc, visited, expl ); + //if we discovered a different cycle while searching this one + if( !cn.isNull() && cn!=eqc ){ + visited.clear(); + expl.clear(); + Node prev = cn; + cn = searchForCycle( cn, cn, visited, expl ); + Assert( prev==cn ); + } - if( !cn.isNull() ) { - Assert( expl.size()>0 ); - d_conflictNode = mkAnd( expl ); - Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - d_conflict = true; - return; + if( !cn.isNull() ) { + Assert( expl.size()>0 ); + d_conflictNode = mkAnd( expl ); + Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + d_conflict = true; + return; + } + }else{ + //indexing + cod_eqc.push_back( eqc ); } } ++eqcs_i; } + //process codatatypes + if( cod_eqc.size()>1 ){ + std::vector< std::vector< Node > > part_out; + std::vector< TNode > exp; + std::map< Node, Node > cn; + std::map< Node, std::map< Node, int > > dni; + for( unsigned i=0; i part; + part.push_back( part_out[i][0] ); + for( unsigned j=1; j > tpart_out; + exp.clear(); + cn.clear(); + cn[part_out[i][0]] = part_out[i][0]; + cn[part_out[i][j]] = part_out[i][j]; + dni.clear(); + separateBisimilar( part, tpart_out, exp, cn, dni, 0, true ); + Assert( tpart_out.size()==1 && tpart_out[0].size()==2 ); + part.pop_back(); + //merge based on explanation + Trace("dt-cod") << " exp is : "; + for( unsigned k=0; k& part, std::vector< std::vector< Node > >& part_out, + std::vector< TNode >& exp, + std::map< Node, Node >& cn, + std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ){ + if( !mkExp ){ + Trace("dt-cod-debug") << "Separate bisimilar : " << std::endl; + for( unsigned i=0; isecond << std::endl; } + new_part_rec[ it_rec->second ].push_back( part[j] ); + }else{ + if( DatatypesRewriter::isTermDatatype( c ) ){ + bool foundCons = false; + EqcInfo* eqc = getOrMakeEqcInfo( c, false ); + if( eqc ){ + Node ncons = eqc->d_constructor.get(); + if( !ncons.isNull() ) { + foundCons = true; + Node cc = ncons.getOperator(); + cn_cons[part[j]] = ncons; + if( mkExp ){ + explainEquality( c, ncons, true, exp ); + } + new_part[cc].push_back( part[j] ); + if( !mkExp ){ Trace("dt-cod-debug") << " - " << part[j] << " is datatype " << ncons << "." << std::endl; } + } + } + if( !foundCons ){ + new_part_c[c].push_back( part[j] ); + if( !mkExp ){ Trace("dt-cod-debug") << " - " << part[j] << " is unspecified datatype." << std::endl; } + } + }else{ + //add equivalences + if( !mkExp ){ Trace("dt-cod-debug") << " - " << part[j] << " is term " << c << "." << std::endl; } + new_part_c[c].push_back( part[j] ); + } + } + } + //direct add for constants + for( std::map< Node, std::vector< Node > >::iterator it = new_part_c.begin(); it != new_part_c.end(); ++it ){ + if( it->second.size()>1 ){ + std::vector< Node > vec; + vec.insert( vec.begin(), it->second.begin(), it->second.end() ); + part_out.push_back( vec ); + } + } + //direct add for recursive + for( std::map< int, std::vector< Node > >::iterator it = new_part_rec.begin(); it != new_part_rec.end(); ++it ){ + if( it->second.size()>1 ){ + std::vector< Node > vec; + vec.insert( vec.begin(), it->second.begin(), it->second.end() ); + part_out.push_back( vec ); + }else{ + //add back : could match a datatype? + } + } + //recurse for the datatypes + for( std::map< Node, std::vector< Node > >::iterator it = new_part.begin(); it != new_part.end(); ++it ){ + if( it->second.size()>1 ){ + //set dni to check for loops + std::map< Node, Node > dni_rem; + for( unsigned i=0; isecond.size(); i++ ){ + Node n = it->second[i]; + dni[n][cn[n]] = dniLvl; + dni_rem[n] = cn[n]; + } + + //we will split based on the arguments of the datatype + std::vector< std::vector< Node > > split_new_part; + split_new_part.push_back( it->second ); + + unsigned nChildren = cn_cons[it->second[0]].getNumChildren(); + //for each child of constructor + unsigned cindex = 0; + while( cindexfirst << "..." << std::endl; } + std::vector< std::vector< Node > > next_split_new_part; + for( unsigned j=0; j > c_part_out; + separateBisimilar( split_new_part[j], c_part_out, exp, cn, dni, dniLvl+1, mkExp ); + next_split_new_part.insert( next_split_new_part.end(), c_part_out.begin(), c_part_out.end() ); + } + split_new_part.clear(); + split_new_part.insert( split_new_part.end(), next_split_new_part.begin(), next_split_new_part.end() ); + cindex++; + } + part_out.insert( part_out.end(), split_new_part.begin(), split_new_part.end() ); + + for( std::map< Node, Node >::iterator it2 = dni_rem.begin(); it2 != dni_rem.end(); ++it2 ){ + dni[it2->first].erase( it2->second ); + } + } + } } //postcondition: if cycle detected, explanation is why n is a subterm of on @@ -1272,8 +1462,7 @@ Node TheoryDatatypes::searchForCycle( Node n, Node on, if( !firstTime ){ nn = getRepresentative( n ); if( nn==on ){ - Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, nn ); - explain( lit, explanation ); + explainEquality( n, nn, true, explanation ); return on; } }else{ @@ -1293,8 +1482,7 @@ Node TheoryDatatypes::searchForCycle( Node n, Node on, //} //add explanation for why the constructor is connected if( n != ncons ) { - Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, ncons ); - explain( lit, explanation ); + explainEquality( n, ncons, true, explanation ); } return on; }else if( !cn.isNull() ){ @@ -1306,7 +1494,13 @@ Node TheoryDatatypes::searchForCycle( Node n, Node on, visited.erase( nn ); return Node::null(); }else{ - return nn; + if( DatatypesRewriter::isTermDatatype( nn ) ) { + const Datatype& dt = ((DatatypeType)(nn.getType()).toType()).getDatatype(); + if( !dt.isCodatatype() ){ + return nn; + } + } + return Node::null(); } } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 2a93878d0..eb8d792cf 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -195,6 +195,9 @@ public: /** propagate */ bool propagate(TNode literal); /** explain */ + void addAssumptions( std::vector& assumptions, std::vector& tassumptions ); + void explainEquality( TNode a, TNode b, bool polarity, std::vector& assumptions ); + void explainPredicate( TNode p, bool polarity, std::vector& assumptions ); void explain( TNode literal, std::vector& assumptions ); Node explain( TNode literal ); /** Conflict when merging two constants */ @@ -236,6 +239,11 @@ private: Node searchForCycle( Node n, Node on, std::map< Node, bool >& visited, std::vector< TNode >& explanation, bool firstTime = true ); + /** for checking whether two codatatype terms must be equal */ + void separateBisimilar( std::vector< Node >& part, std::vector< std::vector< Node > >& part_out, + std::vector< TNode >& exp, + std::map< Node, Node >& cn, + std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ); /** collect terms */ void collectTerms( Node n ); /** get instantiate cons */ diff --git a/src/util/datatype.h b/src/util/datatype.h index 02e0b6be8..a8f3b404a 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -448,6 +448,7 @@ public: private: std::string d_name; std::vector d_params; + bool d_isCo; std::vector d_constructors; bool d_resolved; Type d_self; @@ -494,13 +495,13 @@ private: public: /** Create a new Datatype of the given name. */ - inline explicit Datatype(std::string name); + inline explicit Datatype(std::string name, bool isCo = false); /** * Create a new Datatype of the given name, with the given * parameterization. */ - inline Datatype(std::string name, const std::vector& params); + inline Datatype(std::string name, const std::vector& params, bool isCo = false); /** * Add a constructor to this Datatype. Constructor names need not @@ -526,6 +527,9 @@ public: /** Get parameters */ inline std::vector getParameters() const; + /** is this a co-datatype? */ + inline bool isCodatatype() const; + /** * Return the cardinality of this datatype (the sum of the * cardinalities of its constructors). The Datatype must be @@ -662,18 +666,20 @@ inline std::string DatatypeUnresolvedType::getName() const throw() { return d_name; } -inline Datatype::Datatype(std::string name) : +inline Datatype::Datatype(std::string name, bool isCo) : d_name(name), d_params(), + d_isCo(isCo), d_constructors(), d_resolved(false), d_self(), d_card(CardinalityUnknown()) { } -inline Datatype::Datatype(std::string name, const std::vector& params) : +inline Datatype::Datatype(std::string name, const std::vector& params, bool isCo) : d_name(name), d_params(params), + d_isCo(isCo), d_constructors(), d_resolved(false), d_self(), @@ -707,6 +713,10 @@ inline std::vector Datatype::getParameters() const { return d_params; } +inline bool Datatype::isCodatatype() const { + return d_isCo; +} + inline bool Datatype::operator!=(const Datatype& other) const throw() { return !(*this == other); } -- cgit v1.2.3 From 1138911e0af7c15a7b41a5d02ff3edab2c837449 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Apr 2014 15:36:28 -0500 Subject: Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). Improve datatypes rewrite, make option for previous dt semantics. --- src/theory/datatypes/datatypes_rewriter.h | 66 ++++++++++++++-------------- src/theory/datatypes/options | 4 +- src/theory/datatypes/theory_datatypes.cpp | 10 +++-- src/theory/quantifiers/first_order_model.cpp | 15 ++++++- src/theory/quantifiers/full_model_check.cpp | 2 +- test/regress/regress0/fmf/Makefile.am | 5 ++- 6 files changed, 60 insertions(+), 42 deletions(-) diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 8cb3fb4a2..99245ef69 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -138,26 +138,25 @@ public: << std::endl; return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); }else{ - if( options::dtRewriteErrorSel() ){ - Node gt; - if( in.getType().isSort() ){ - TypeEnumerator te(in.getType()); - gt = *te; - }else{ - gt = in.getType().mkGroundTerm(); - } - TypeNode gtt = gt.getType(); - //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); - if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){ - gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); - } - Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " - << "Rewrite trivial selector " << in - << " to distinguished ground term " - << in.getType().mkGroundTerm() << std::endl; - return RewriteResponse(REWRITE_DONE,gt ); + //typically should not be called + Node gt; + if( in.getType().isSort() ){ + TypeEnumerator te(in.getType()); + gt = *te; + }else{ + gt = in.getType().mkGroundTerm(); } + TypeNode gtt = gt.getType(); + //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); + if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){ + gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); + } + Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + << "Rewrite trivial selector " << in + << " to distinguished ground term " + << in.getType().mkGroundTerm() << std::endl; + return RewriteResponse(REWRITE_DONE,gt ); } } if(in.getKind() == kind::TUPLE_SELECT && @@ -204,11 +203,18 @@ public: return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } - if(in.getKind() == kind::EQUAL && - checkClash(in[0], in[1])) { - Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl; - return RewriteResponse(REWRITE_DONE, - NodeManager::currentNM()->mkConst(false)); + if(in.getKind() == kind::EQUAL ) { + std::vector< Node > rew; + if( checkClash(in[0], in[1], rew) ){ + Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl; + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(false)); + }else if( rew.size()!=1 || rew[0]!=in ){ + Node nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) : + ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); + Trace("datatypes-rewrite") << "Rewrite equality to " << nn << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, nn ); + } } return RewriteResponse(REWRITE_DONE, in); @@ -222,7 +228,7 @@ public: static inline void init() {} static inline void shutdown() {} - static bool checkClash( Node n1, Node n2 ) { + static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) { if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) || (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) || (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) { @@ -231,18 +237,14 @@ public: } else { Assert( n1.getNumChildren() == n2.getNumChildren() ); for( int i=0; i<(int)n1.getNumChildren(); i++ ) { - if( checkClash( n1[i], n2[i] ) ) { + if( checkClash( n1[i], n2[i], rew ) ) { return true; } } } - }else if( !isTermDatatype( n1 ) ){ - //also check for clashes between non-datatypes + }else{ Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); - eq = Rewriter::rewrite( eq ); - if( eq==NodeManager::currentNM()->mkConst(false) ){ - return true; - } + rew.push_back( eq ); } return false; } diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options index 1daa30981..fcf36648d 100644 --- a/src/theory/datatypes/options +++ b/src/theory/datatypes/options @@ -9,8 +9,8 @@ module DATATYPES "theory/datatypes/options.h" Datatypes theory # then we do not rewrite such a selector term to an arbitrary ground term. # For example, by default cvc4 considers cdr( nil ) = nil. If this option is set, then # cdr( nil ) has no set value. -expert-option dtRewriteErrorSel /--disable-dt-rewrite-error-sel bool :default true - disable rewriting incorrectly applied selectors to arbitrary ground term +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 diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index fc37c5417..4858d99db 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -327,15 +327,18 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { switch( n.getKind() ){ case kind::APPLY_SELECTOR: { - Node selector = n.getOperator(); - Expr selectorExpr = selector.toExpr(); + Node selector = n.getOperator(); + Expr selectorExpr = selector.toExpr(); + Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] ); + if( options::dtRewriteErrorSel() ){ + return sel; + }else{ size_t selectorIndex = Datatype::cindexOf(selectorExpr); const Datatype& dt = Datatype::datatypeOf(selectorExpr); const DatatypeConstructor& c = dt[selectorIndex]; Expr tester = c.getTester(); Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] ); tst = Rewriter::rewrite( tst ); - Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] ); Node n_ret; if( tst==NodeManager::currentNM()->mkConst( true ) ){ n_ret = sel; @@ -357,6 +360,7 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { Trace("dt-expand") << "Expand def : " << n << " to " << n_ret << std::endl; return n_ret; } + } break; default: return n; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 54be11b44..d5c2b0e9d 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -648,7 +648,18 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); Node curr; for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) { - Node v = getRepresentative( d_models[op]->d_value[i] ); + Node v = d_models[op]->d_value[i]; + if( !hasTerm( v ) ){ + //can happen when the model basis term does not exist in ground assignment + TypeNode tn = v.getType(); + if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){ + //see full_model_check.cpp line 366 + v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ]; + }else{ + Assert( false ); + } + } + v = getRepresentative( v ); if( curr.isNull() ){ curr = v; }else{ @@ -664,7 +675,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { if( !isStar(cond[j][1]) ){ children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) ); } - }else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground representatives of this type... + }else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground eqc of this type d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){ Node c = getUsedRepresentative( cond[j] ); children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 6c889781d..126b30b81 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -937,7 +937,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n void FullModelChecker::doNegate( Def & dc ) { for (unsigned i=0; i Date: Thu, 17 Apr 2014 04:24:11 -0500 Subject: Minor refactoring and optimizing. --- src/theory/datatypes/datatypes_rewriter.h | 52 +++++++++++++++++++++++++++++++ src/theory/datatypes/theory_datatypes.cpp | 50 +++++++---------------------- src/theory/datatypes/theory_datatypes.h | 2 +- 3 files changed, 64 insertions(+), 40 deletions(-) diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 99245ef69..e884248e7 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -248,6 +248,58 @@ public: } return false; } + /** get instantiate cons */ + static Node getInstCons( Node n, const Datatype& dt, int index, bool mkVar = false ) { + Type tspec; + if( dt.isParametric() ){ + tspec = dt[index].getSpecializedConstructorType(n.getType().toType()); + } + std::vector< Node > children; + children.push_back( Node::fromExpr( dt[index].getConstructor() ) ); + for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){ + Node nc = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), n ); + if( mkVar ){ + TypeNode tn = nc.getType(); + if( dt.isParametric() ){ + tn = TypeNode::fromType( tspec )[i]; + } + nc = NodeManager::currentNM()->mkSkolem( "m_$$", tn, "created for inst cons" ); + } + children.push_back( nc ); + } + Node n_ic = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); + //add type ascription for ambiguous constructor types + if(!n_ic.getType().isComparableTo(n.getType())) { + Assert( dt.isParametric() ); + Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl; + Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl; + Type tspec = dt[index].getSpecializedConstructorType(n.getType().toType()); + Debug("datatypes-parametric") << "Type specification is " << tspec << std::endl; + children[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(tspec)), children[0] ); + n_ic = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); + Assert( n_ic.getType()==n.getType() ); + } + Assert( isInstCons( n_ic, dt, index ) ); + //n_ic = Rewriter::rewrite( n_ic ); + return n_ic; + } + static bool isInstCons( Node n, const Datatype& dt, int index ){ + if( n.getKind()==kind::APPLY_CONSTRUCTOR ){ + const DatatypeConstructor& c = dt[index]; + if( n.getOperator()==Node::fromExpr( c.getConstructor() ) ){ + for( unsigned i=0; i::iterator it = d_inst_map[n].find( index ); + if( it!=d_inst_map[n].end() ){ + return it->second; + }else{ //add constructor to equivalence class - Type tspec; - if( dt.isParametric() ){ - tspec = dt[index].getSpecializedConstructorType(n.getType().toType()); - } - std::vector< Node > children; - children.push_back( Node::fromExpr( dt[index].getConstructor() ) ); - for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){ - Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), n ); - if( mkVar ){ - TypeNode tn = nc.getType(); - if( dt.isParametric() ){ - tn = TypeNode::fromType( tspec )[i]; - } - nc = NodeManager::currentNM()->mkSkolem( "m_$$", tn, "created during model gen" ); - } - children.push_back( nc ); - if( isActive ){ - processNewTerm( nc ); - } - } - Node n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + Node n_ic = DatatypesRewriter::getInstCons( n, dt, index, mkVar ); if( isActive ){ + for( unsigned i = 0; imkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(tspec)), children[0] ); - n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); - Assert( n_ic.getType()==n.getType() ); - } n_ic = Rewriter::rewrite( n_ic ); Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl; - //d_inst_map[n][index] = n_ic; + d_inst_map[n][index] = n_ic; return n_ic; - //} + } } void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ @@ -1238,7 +1210,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ //if( eqc->d_selectors || dt[ index ].isFinite() ){ // || mustSpecifyAssignment() //instantiate this equivalence class eqc->d_inst = true; - Node tt_cons = getInstantiateCons( tt, dt, index ); + Node tt_cons = getInstantiateCons( tt, dt, index, false, true ); Node eq; if( tt!=tt_cons ){ eq = tt.eqNode( tt_cons ); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index eb8d792cf..307e90e91 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -247,7 +247,7 @@ private: /** collect terms */ void collectTerms( Node n ); /** get instantiate cons */ - Node getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar = false, bool isActive = true ); + Node getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar, bool isActive ); /** process new term that was created internally */ void processNewTerm( Node n ); /** check instantiate */ -- cgit v1.2.3 From e77289614a61d8658f8fc56073fa3334c14139b8 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 17 Apr 2014 15:16:42 -0400 Subject: Allow fmf-bound-int to be set with set-option and via API. --- src/theory/quantifiers/options | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index b7f015f47..32e65438e 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -112,7 +112,7 @@ option fmfFreshDistConst --fmf-fresh-dc bool :default false use fresh distinguished representative when applying Inst-Gen techniques option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding -option fmfBoundInt --fmf-bound-int bool :default false :read-write +option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write finite model finding on bounded integer quantification option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" -- cgit v1.2.3 From 766859010a5ca2cc94ffe69908dfe2606df2af28 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 22 Apr 2014 03:16:56 -0500 Subject: Minor fix to avoid rewriting datatype equalities into non-equalitiers, as required. Add APPLY_UF to congruence types to avoid model construction bugs. --- src/theory/datatypes/datatypes_rewriter.h | 13 +++++-------- src/theory/datatypes/theory_datatypes.cpp | 15 +++++++++++++++ 2 files changed, 20 insertions(+), 8 deletions(-) diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index e884248e7..75d1f2b2e 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -207,13 +207,10 @@ public: std::vector< Node > rew; if( checkClash(in[0], in[1], rew) ){ Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl; - return RewriteResponse(REWRITE_DONE, - NodeManager::currentNM()->mkConst(false)); - }else if( rew.size()!=1 || rew[0]!=in ){ - Node nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) : - ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); - Trace("datatypes-rewrite") << "Rewrite equality to " << nn << std::endl; - return RewriteResponse(REWRITE_AGAIN_FULL, nn ); + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false)); + }else if( rew.size()==1 && rew[0]!=in ){ + Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " << rew[0] << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] ); } } @@ -242,7 +239,7 @@ public: } } } - }else{ + }else if( n1!=n2 ){ Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); rew.push_back( eq ); } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 8afcbb1de..2fb1a2679 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -56,6 +56,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); + d_equalityEngine.addFunctionKind(kind::APPLY_UF); } TheoryDatatypes::~TheoryDatatypes() { @@ -412,6 +413,19 @@ Node TheoryDatatypes::ppRewrite(TNode in) { NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr())); } } + + if( in.getKind()==EQUAL ){ + Node nn; + std::vector< Node > rew; + if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){ + nn = NodeManager::currentNM()->mkConst(false); + }else{ + nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) : + ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); + } + return nn; + } + // nothing to do return in; } @@ -465,6 +479,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { Assert(!n.isNull()); + Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl; return n; -- cgit v1.2.3 From bd3a86055008e692ac4e5e6fa5dfce9e78660d8a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 24 Apr 2014 03:35:08 -0500 Subject: Add --inst-max-level=N option for Kshitij. Support define-const command in Smt2. --- src/parser/smt2/Smt2.g | 25 ++++++++++++++++++++++++- src/theory/quantifiers/options | 2 ++ src/theory/quantifiers_engine.cpp | 35 ++++++++++++++++++++++------------- 3 files changed, 48 insertions(+), 14 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 2118a240d..8dcebc5ee 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -344,6 +344,28 @@ command returns [CVC4::Command* cmd = NULL] Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); $cmd = new DefineFunctionCommand(name, func, terms, expr); } + | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + sortSymbol[t,CHECK_DECLARED] + { /* add variables to parser state before parsing term */ + Debug("parser") << "define const: '" << name << "'" << std::endl; + PARSER_STATE->pushScope(true); + for(std::vector >::const_iterator i = + sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; + ++i) { + terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); + } + } + term[expr, expr2] + { PARSER_STATE->popScope(); + // declare the name down here (while parsing term, signature + // must not be extended with the name itself; no recursion + // permitted) + Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); + $cmd = new DefineFunctionCommand(name, func, terms, expr); + } | /* value query */ GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK @@ -487,7 +509,7 @@ extendedCommand[CVC4::Command*& cmd] sortSymbol[t,CHECK_DECLARED] { Expr c = PARSER_STATE->mkVar(name, t); $cmd = new DeclareFunctionCommand(name, c, t); } - + | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); } { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) && @@ -1645,6 +1667,7 @@ DECLARE_FUNS_TOK : 'declare-funs'; DECLARE_PREDS_TOK : 'declare-preds'; DEFINE_TOK : 'define'; DECLARE_CONST_TOK : 'declare-const'; +DEFINE_CONST_TOK : 'define-const'; SIMPLIFY_TOK : 'simplify'; INCLUDE_TOK : 'include'; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 32e65438e..e733764f0 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -67,6 +67,8 @@ option registerQuantBodyTerms --register-quant-body-terms bool :default false option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" when to apply instantiation +option instMaxLevel --inst-max-level=N int :default -1 + maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index eaf5e8228..63697f5e7 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -319,7 +319,6 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std Trace("inst") << " " << terms[i]; Trace("inst") << std::endl; } - //uint64_t maxInstLevel = 0; if( options::cbqi() ){ for( int i=0; i<(int)terms.size(); i++ ){ if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){ @@ -328,22 +327,21 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std Debug("inst") << " " << terms[i] << std::endl; } Unreachable("Bad instantiation"); - }else{ - Trace("inst") << " " << terms[i]; - //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute()); - Trace("inst") << std::endl; - //if( terms[i].hasAttribute(InstLevelAttribute()) ){ - //if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ - // maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); - //} - //}else{ - //setInstantiationLevelAttr( terms[i], 0 ); - //} } } } + if( options::instMaxLevel()!=-1 ){ + uint64_t maxInstLevel = 0; + for( int i=0; i<(int)terms.size(); i++ ){ + if( terms[i].hasAttribute(InstLevelAttribute()) ){ + if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ + maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); + } + } + } + setInstantiationLevelAttr( body, maxInstLevel+1 ); + } Trace("inst-debug") << "*** Lemma is " << lem << std::endl; - //setInstantiationLevelAttr( body, maxInstLevel+1 ); ++(d_statistics.d_instantiations); return true; }else{ @@ -504,6 +502,17 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo } Trace("inst-add-debug") << std::endl; + if( options::instMaxLevel()!=-1 ){ + for( unsigned i=0; ioptions::instMaxLevel() ){ + Trace("inst-add-debug") << "Term " << terms[i] << " has instantiation level " << terms[i].getAttribute(InstLevelAttribute()); + Trace("inst-add-debug") << ", which is more than maximum allowed level " << options::instMaxLevel() << std::endl; + return false; + } + } + } + //check for duplication ///* bool alreadyExists = false; -- cgit v1.2.3 From d132321d74b65b293ffac4bc8c6f0d8db73614d6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 24 Apr 2014 14:27:38 +0200 Subject: Compute care graph for datatypes. Preliminary results show 20x speed up on larger problems. Improve datatypes rewriter. --- src/theory/datatypes/datatypes_rewriter.h | 10 ++++-- src/theory/datatypes/theory_datatypes.cpp | 54 +++++++++++++++++++++++++++---- src/theory/datatypes/theory_datatypes.h | 12 ++++--- 3 files changed, 64 insertions(+), 12 deletions(-) diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 75d1f2b2e..dc85d0cd6 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -211,6 +211,8 @@ public: }else if( rew.size()==1 && rew[0]!=in ){ Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " << rew[0] << std::endl; return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] ); + }else{ + Trace("datatypes-rewrite-debug") << "Did not rewrite equality " << in << " " << in[0].getKind() << " " << in[1].getKind() << std::endl; } } @@ -240,8 +242,12 @@ public: } } }else if( n1!=n2 ){ - Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); - rew.push_back( eq ); + if( n1.isConst() && n2.isConst() ){ + return true; + }else{ + Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); + rew.push_back( eq ); + } } return false; } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 2fb1a2679..e706d3846 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -50,7 +50,9 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_labels( c ), d_selector_apps( c ), d_conflict( c, false ), - d_collectTermsCache( c ){ + d_collectTermsCache( c ), + d_consTerms( c ), + d_selTerms( c ){ // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); @@ -963,7 +965,45 @@ EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){ } void TheoryDatatypes::computeCareGraph(){ - Theory::computeCareGraph(); + Trace("ajr-temp") << "Compute graph for dt..." << std::endl; + vector< pair > currentPairs; + for( unsigned r=0; r<2; r++ ){ + unsigned functionTerms = r==0 ? d_consTerms.size() : d_selTerms.size(); + for( unsigned i=0; i d_pending_merge; /** expand definition skolem functions */ std::map< Node, Node > d_exp_def_skolem; + /** All the constructor terms that the theory has seen */ + context::CDList d_consTerms; + /** All the selector terms that the theory has seen */ + context::CDList d_selTerms; private: /** assert fact */ void assertFact( Node fact, Node exp ); @@ -261,10 +265,10 @@ private: bool mustCommunicateFact( Node n, Node exp ); private: //equality queries - bool hasTerm( Node a ); - bool areEqual( Node a, Node b ); - bool areDisequal( Node a, Node b ); - Node getRepresentative( Node a ); + bool hasTerm( TNode a ); + bool areEqual( TNode a, TNode b ); + bool areDisequal( TNode a, TNode b ); + Node getRepresentative( TNode a ); public: /** get equality engine */ eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; } -- cgit v1.2.3 From 9a4df62fbb05a09c95877b53053ff2e231ae254c Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 24 Apr 2014 16:47:46 +0200 Subject: Avoid assigning constructor terms to 1-constructor datatype eqcs, when possible, to ensure termination for codatatypes. Minor changes. --- src/theory/datatypes/theory_datatypes.cpp | 159 ++++++++++++++++-------------- 1 file changed, 85 insertions(+), 74 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index e706d3846..eef25ca80 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -150,61 +150,63 @@ void TheoryDatatypes::check(Effort e) { if( eqc->d_constructor.get().isNull() && !hasLabel( eqc, n ) ) { Trace("datatypes-debug") << "No constructor..." << std::endl; const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); - //if only one constructor, then this term must be this constructor - if( dt.getNumConstructors()==1 ){ - Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n ); - d_pending.push_back( t ); - d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true ); - Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl; - d_infer.push_back( t ); - }else{ - std::vector< bool > pcons; - getPossibleCons( eqc, n, pcons ); - //std::cout << "pcons " << n << " = "; - //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; } - //std::cout << std::endl; - //check if we do not need to resolve the constructor type for this equivalence class. - // this is if there are no selectors for this equivalence class, its possible values are infinite, - // and we are not producing a model, then do not split. - int consIndex = -1; - bool needSplit = true; - for( unsigned int j=0; jd_selectors ) { - needSplit = false; - } + + std::vector< bool > pcons; + getPossibleCons( eqc, n, pcons ); + //std::cout << "pcons " << n << " = "; + //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; } + //std::cout << std::endl; + //check if we do not need to resolve the constructor type for this equivalence class. + // this is if there are no selectors for this equivalence class, its possible values are infinite, + // and we are not producing a model, then do not split. + int consIndex = -1; + bool needSplit = true; + for( unsigned int j=0; jd_selectors ) { + needSplit = false; } - needSplit = true; } - */ - if( needSplit && consIndex!=-1 ) { - 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 ); - return; + } + /* + if( !needSplit && mustSpecifyAssignment() ){ + //for the sake of termination, we must choose the constructor of a ground term + //NEED GUARENTEE: groundTerm should not contain any subterms of the same type + // TODO: this is probably not good enough, actually need fair enumeration strategy + Node groundTerm = n.getType().mkGroundTerm(); + int index = Datatype::indexOf( groundTerm.getOperator().toExpr() ); + if( pcons[index] ){ + consIndex = index; + } + needSplit = true; + } + */ + if( needSplit && consIndex!=-1 ) { + //if only one constructor, then this term must be this constructor + if( dt.getNumConstructors()==1 ){ + Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n ); + d_pending.push_back( t ); + d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true ); + Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl; + d_infer.push_back( t ); }else{ - Trace("dt-split-debug") << "Do not split constructor for " << n << std::endl; + 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 ); + return; } + }else{ + Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl; } + }else{ Trace("datatypes-debug") << "Has constructor " << eqc->d_constructor.get() << std::endl; } @@ -965,7 +967,7 @@ EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){ } void TheoryDatatypes::computeCareGraph(){ - Trace("ajr-temp") << "Compute graph for dt..." << std::endl; + Trace("dt-cg") << "Compute graph for dt..." << std::endl; vector< pair > currentPairs; for( unsigned r=0; r<2; r++ ){ unsigned functionTerms = r==0 ? d_consTerms.size() : d_selTerms.size(); @@ -974,7 +976,7 @@ void TheoryDatatypes::computeCareGraph(){ for( unsigned j=i+1; jareEqual( cons[i][j], neqc[j] ) ){ - diff = true; + //if it is infinite or we are assigning to terms known by datatypes, make sure it is fresh + if( eqc.getType().getCardinality().isInfinite() || indexareEqual( cons[i][j], neqc[j] ) ){ + diff = true; + break; + } + } + if( !diff ){ + Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; + success = false; break; } } - if( !diff ){ - Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; - success = false; - break; - } } } }while( !success ); @@ -1133,6 +1143,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ for( unsigned r=0; r<2; r++ ){ if( neqc.isNull() ){ for( unsigned i=0; i Date: Thu, 24 Apr 2014 17:30:15 -0500 Subject: minor change: add a heuristic for preventing constant splitting. --- src/theory/strings/theory_strings.cpp | 59 +++++++++++++++++--------- src/theory/strings/theory_strings.h | 5 ++- src/util/regexp.cpp | 80 +++++++++++++++++++++++++++++++++++ src/util/regexp.h | 74 +++++--------------------------- 4 files changed, 133 insertions(+), 85 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index f2172071d..d03faa72a 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -65,7 +65,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_curr_cardinality(c, 0) { // The kinds we are treating as function application in congruence - //d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); + d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); d_equalityEngine.addFunctionKind(kind::STRING_CONCAT); d_equalityEngine.addFunctionKind(kind::STRING_STRCTN); @@ -418,7 +418,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { break; case kind::STRING_IN_REGEXP: //do not add trigger here - //d_equalityEngine.addTriggerPredicate(n); + d_equalityEngine.addTriggerPredicate(n); break; case kind::STRING_SUBSTR_TOTAL: { Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, @@ -560,7 +560,7 @@ void TheoryStrings::check(Effort e) { //must record string in regular expressions if ( atom.getKind() == kind::STRING_IN_REGEXP ) { addMembership(assertion); - //d_equalityEngine.assertPredicate(atom, polarity, fact); + d_equalityEngine.assertPredicate(atom, polarity, fact); } else if (atom.getKind() == kind::STRING_STRCTN) { if(polarity) { d_str_pos_ctn.push_back( atom ); @@ -1232,18 +1232,37 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." ); Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." ); antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - Node firstChar = const_str.getConst().size() == 1 ? const_str : - NodeManager::currentNM()->mkConst( const_str.getConst().substr(0, 1) ); - //split the string - Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) ); - Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false ); - d_pending_req_phase[ eq1 ] = true; - conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); - Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; - - Node ant = mkExplain( antec ); - sendLemma( ant, conc, "CST-SPLIT" ); - ++(d_statistics.d_eq_splits); + //Opt + bool optflag = false; + if( normal_forms[nconst_k].size() > nconst_index_k + 1 && + normal_forms[nconst_k][nconst_index_k + 1].isConst() ) { + CVC4::String stra = const_str.getConst(); + CVC4::String strb = normal_forms[nconst_k][nconst_index_k + 1].getConst(); + CVC4::String fc = strb.substr(0, 1); + if( stra.find(fc) == std::string::npos || + (stra.find(strb) == std::string::npos && + !stra.overlap(strb)) ) { + Node sk = NodeManager::currentNM()->mkSkolem( "sopt_$$", NodeManager::currentNM()->stringType(), "created for string sp" ); + Node eq = other_str.eqNode( mkConcat(const_str, sk) ); + Node ant = mkExplain( antec ); + sendLemma(ant, eq, "CST-EPS"); + optflag = true; + } + } + if(!optflag){ + Node firstChar = const_str.getConst().size() == 1 ? const_str : + NodeManager::currentNM()->mkConst( const_str.getConst().substr(0, 1) ); + //split the string + Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) ); + Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false ); + d_pending_req_phase[ eq1 ] = true; + conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; + + Node ant = mkExplain( antec ); + sendLemma( ant, conc, "CST-SPLIT" ); + ++(d_statistics.d_eq_splits); + } return true; } else { std::vector< Node > antec_new_lits; @@ -1785,10 +1804,7 @@ void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) { } Node TheoryStrings::mkConcat( Node n1, Node n2 ) { - std::vector< Node > c; - c.push_back( n1 ); - c.push_back( n2 ); - return mkConcat( c ); + return NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 ); } Node TheoryStrings::mkConcat( std::vector< Node >& c ) { @@ -2888,6 +2904,11 @@ void TheoryStrings::addMembership(Node assertion) { d_regexp_memberships.push_back( assertion ); } +Node TheoryStrings::instantiateSymRegExp(Node r) { + //TODO: + return r; +} + //// Finite Model Finding Node TheoryStrings::getNextDecisionRequest() { diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 9f99012df..33283d1cf 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -272,8 +272,8 @@ protected: void sendInfer( Node eq_exp, Node eq, const char * c ); void sendSplit( Node a, Node b, const char * c, bool preq = true ); /** mkConcat **/ - Node mkConcat( Node n1, Node n2 ); - Node mkConcat( std::vector< Node >& c ); + inline Node mkConcat( Node n1, Node n2 ); + inline Node mkConcat( std::vector< Node >& c ); /** mkExplain **/ Node mkExplain( std::vector< Node >& a ); Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); @@ -323,6 +323,7 @@ private: bool splitRegExp( Node x, Node r, Node ant ); bool addMembershipLength(Node atom); void addMembership(Node assertion); + Node instantiateSymRegExp(Node r); // Finite Model Finding diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index b6db624d5..3bc17b050 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -23,6 +23,71 @@ using namespace std; namespace CVC4 { +void String::toInternal(const std::string &s) { + d_str.clear(); + unsigned i=0; + while(i < s.size()) { + if(s[i] == '\\') { + i++; + if(i < s.size()) { + switch(s[i]) { + case 'n': {d_str.push_back( convertCharToUnsignedInt('\n') );i++;} break; + case 't': {d_str.push_back( convertCharToUnsignedInt('\t') );i++;} break; + case 'v': {d_str.push_back( convertCharToUnsignedInt('\v') );i++;} break; + case 'b': {d_str.push_back( convertCharToUnsignedInt('\b') );i++;} break; + case 'r': {d_str.push_back( convertCharToUnsignedInt('\r') );i++;} break; + case 'f': {d_str.push_back( convertCharToUnsignedInt('\f') );i++;} break; + case 'a': {d_str.push_back( convertCharToUnsignedInt('\a') );i++;} break; + case '\\': {d_str.push_back( convertCharToUnsignedInt('\\') );i++;} break; + case 'x': { + if(i + 2 < s.size()) { + if((isdigit(s[i+1]) || (s[i+1] >= 'a' && s[i+1] >= 'f') || (s[i+1] >= 'A' && s[i+1] >= 'F')) && + (isdigit(s[i+2]) || (s[i+2] >= 'a' && s[i+2] >= 'f') || (s[i+2] >= 'A' && s[i+2] >= 'F'))) { + d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) ); + i += 3; + } else { + throw CVC4::Exception( "Error String Literal: \"" + s + "\"" ); + } + } else { + throw CVC4::Exception( "Error String Literal: \"" + s + "\"" ); + } + } + break; + default: { + if(isdigit(s[i])) { + int num = (int)s[i] - (int)'0'; + bool flag = num < 4; + if(i+1 < s.size() && num < 8 && isdigit(s[i+1]) && s[i+1] < '8') { + num = num * 8 + (int)s[i+1] - (int)'0'; + if(flag && i+2 < s.size() && isdigit(s[i+2]) && s[i+2] < '8') { + num = num * 8 + (int)s[i+2] - (int)'0'; + d_str.push_back( convertCharToUnsignedInt((char)num) ); + i += 3; + } else { + d_str.push_back( convertCharToUnsignedInt((char)num) ); + i += 2; + } + } else { + d_str.push_back( convertCharToUnsignedInt((char)num) ); + i++; + } + } else { + d_str.push_back( convertCharToUnsignedInt(s[i]) ); + i++; + } + } + } + } else { + throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" ); + //d_str.push_back( convertCharToUnsignedInt('\\') ); + } + } else { + d_str.push_back( convertCharToUnsignedInt(s[i]) ); + i++; + } + } +} + void String::getCharSet(std::set &cset) const { for(std::vector::const_iterator itr = d_str.begin(); itr != d_str.end(); itr++) { @@ -30,6 +95,21 @@ void String::getCharSet(std::set &cset) const { } } +bool String::overlap(String &y) const { + unsigned n = y.size(); + if(d_str.size() < y.size()) { + n = d_str.size(); + } + for(unsigned i=1; i= 'a' && s[i+1] >= 'f') || (s[i+1] >= 'A' && s[i+1] >= 'F')) && - (isdigit(s[i+2]) || (s[i+2] >= 'a' && s[i+2] >= 'f') || (s[i+2] >= 'A' && s[i+2] >= 'F'))) { - d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) ); - i += 3; - } else { - throw CVC4::Exception( "Error String Literal: \"" + s + "\"" ); - } - } else { - throw CVC4::Exception( "Error String Literal: \"" + s + "\"" ); - } - } - break; - default: { - if(isdigit(s[i])) { - int num = (int)s[i] - (int)'0'; - bool flag = num < 4; - if(i+1 < s.size() && num < 8 && isdigit(s[i+1]) && s[i+1] < '8') { - num = num * 8 + (int)s[i+1] - (int)'0'; - if(flag && i+2 < s.size() && isdigit(s[i+2]) && s[i+2] < '8') { - num = num * 8 + (int)s[i+2] - (int)'0'; - d_str.push_back( convertCharToUnsignedInt((char)num) ); - i += 3; - } else { - d_str.push_back( convertCharToUnsignedInt((char)num) ); - i += 2; - } - } else { - d_str.push_back( convertCharToUnsignedInt((char)num) ); - i++; - } - } else { - d_str.push_back( convertCharToUnsignedInt(s[i]) ); - i++; - } - } - } - } else { - throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" ); - //d_str.push_back( convertCharToUnsignedInt('\\') ); - } - } else { - d_str.push_back( convertCharToUnsignedInt(s[i]) ); - i++; - } - } - } + void toInternal(const std::string &s); public: String() {} @@ -316,6 +253,15 @@ public: ret_vec.insert( ret_vec.end(), itr, itr + j ); return String(ret_vec); } + + String prefix(unsigned i) const { + return substr(0, i); + } + String suffix(unsigned i) const { + return substr(d_str.size() - i, i); + } + bool overlap(String &y) const; + bool isNumber() const { if(d_str.size() == 0) return false; for(unsigned int i=0; i