From bd3a86055008e692ac4e5e6fa5dfce9e78660d8a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 24 Apr 2014 03:35:08 -0500 Subject: [PATCH] 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; -- 2.30.2