This was a feature implemented for "Deciding Local Theory Extensions via E-matching" CAV 2015 that is not used anymore, and will be a burden to maintain further with potential changes to term database.
It also simplifies the TermDatabase::addTerm method (which changed indentation).
{FORALL, CVC4::Kind::FORALL},
{EXISTS, CVC4::Kind::EXISTS},
{BOUND_VAR_LIST, CVC4::Kind::BOUND_VAR_LIST},
- {INST_CLOSURE, CVC4::Kind::INST_CLOSURE},
{INST_PATTERN, CVC4::Kind::INST_PATTERN},
{INST_NO_PATTERN, CVC4::Kind::INST_NO_PATTERN},
{INST_ATTRIBUTE, CVC4::Kind::INST_ATTRIBUTE},
{CVC4::Kind::FORALL, FORALL},
{CVC4::Kind::EXISTS, EXISTS},
{CVC4::Kind::BOUND_VAR_LIST, BOUND_VAR_LIST},
- {CVC4::Kind::INST_CLOSURE, INST_CLOSURE},
{CVC4::Kind::INST_PATTERN, INST_PATTERN},
{CVC4::Kind::INST_NO_PATTERN, INST_NO_PATTERN},
{CVC4::Kind::INST_ATTRIBUTE, INST_ATTRIBUTE},
* mkTerm(Kind kind, const std::vector<Term>& children)
*/
BOUND_VAR_LIST,
- /*
- * A predicate for specifying term in instantiation closure.
- * Parameters: 1
- * -[1]: Term
- * Create with:
- * mkTerm(Kind kind, Term child)
- */
- INST_CLOSURE,
/*
* An instantiation pattern.
* Specifies a (list of) terms to be used as a pattern for quantifier
default = "true"
help = "compute inverse for concat over equalities rather than producing an invertibility condition"
-### Local theory extensions options
-
-[[option]]
- name = "lteRestrictInstClosure"
- category = "regular"
- long = "lte-restrict-inst-closure"
- type = "bool"
- default = "false"
- read_only = true
- help = "treat arguments of inst closure as restricted terms for instantiation"
-
### Reduction options
[[option]]
void Smt2::addQuantifiersOperators()
{
- if (!strictModeEnabled())
- {
- addOperator(api::INST_CLOSURE, "inst-closure");
- }
}
void Smt2::addBitvectorOperators() {
if( n.getType().isComparableTo( d_match_pattern_type ) ){
TNode nh = tdb->getEligibleTermInEqc(n);
if( !nh.isNull() ){
- if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
+ if (options::instMaxLevel() != -1)
+ {
nh = d_qe->getInternalRepresentative( nh, d_f, d_index );
//don't consider this if already the instantiation is ineligible
if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f))
return -2;
}else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type
return -2;
- }
- else if (options::lteRestrictInstClosure()
- && (!d_tdb->isInstClosure(n) || !d_tdb->hasTermCurrent(n, false)))
- {
- return -1;
}else if( options::instMaxLevel()!=-1 ){
//score prefer lowest instantiation level
if( n.hasAttribute(InstLevelAttribute()) ){
}
// check based on instantiation level
- if (options::instMaxLevel() != -1 || options::lteRestrictInstClosure())
+ if (options::instMaxLevel() != -1)
{
for (Node& t : terms)
{
# a list of instantiation patterns
operator INST_PATTERN_LIST 1: "a list of instantiation patterns"
-operator INST_CLOSURE 1 "predicate for specifying term in instantiation closure."
-
typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule
typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule
typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule
typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule
typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule
typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule
-typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule
-typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule
+typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule
endtheory
}
}
-void TermDb::addTerm(Node n,
- std::set<Node>& added,
- bool withinQuant,
- bool withinInstClosure)
+void TermDb::addTerm(Node n)
{
- //don't add terms in quantifier bodies
- if( withinQuant && !options::registerQuantBodyTerms() ){
+ if (d_processed.find(n) != d_processed.end())
+ {
return;
}
- bool rec = false;
- if (d_processed.find(n) == d_processed.end())
+ d_processed.insert(n);
+ if (!TermUtil::hasInstConstAttr(n))
{
- d_processed.insert(n);
- if (!TermUtil::hasInstConstAttr(n))
+ Trace("term-db-debug") << "register term : " << n << std::endl;
+ d_type_map[n.getType()].push_back(n);
+ // if this is an atomic trigger, consider adding it
+ if (inst::TriggerTermInfo::isAtomicTrigger(n))
{
- Trace("term-db-debug") << "register term : " << n << std::endl;
- d_type_map[n.getType()].push_back(n);
- // if this is an atomic trigger, consider adding it
- if (inst::TriggerTermInfo::isAtomicTrigger(n))
- {
- Trace("term-db") << "register term in db " << n << std::endl;
+ Trace("term-db") << "register term in db " << n << std::endl;
- Node op = getMatchOperator(n);
- Trace("term-db-debug") << " match operator is : " << op << std::endl;
- if (d_op_map.find(op) == d_op_map.end())
- {
- d_ops.push_back(op);
- }
- d_op_map[op].push_back(n);
- added.insert(n);
- // If we are higher-order, we may need to register more terms.
- if (options::ufHo())
- {
- addTermHo(n, added, withinQuant, withinInstClosure);
- }
+ Node op = getMatchOperator(n);
+ Trace("term-db-debug") << " match operator is : " << op << std::endl;
+ if (d_op_map.find(op) == d_op_map.end())
+ {
+ d_ops.push_back(op);
+ }
+ d_op_map[op].push_back(n);
+ // If we are higher-order, we may need to register more terms.
+ if (options::ufHo())
+ {
+ addTermHo(n);
}
}
- else
- {
- setTermInactive(n);
- }
- rec = true;
}
- if (withinInstClosure
- && d_iclosure_processed.find(n) == d_iclosure_processed.end())
+ else
{
- d_iclosure_processed.insert(n);
- rec = true;
+ setTermInactive(n);
}
- if (rec && !n.isClosure())
+ if (!n.isClosure())
{
for (const Node& nc : n)
{
- addTerm(nc, added, withinQuant, withinInstClosure);
+ addTerm(nc);
}
}
}
}
}
-void TermDb::addTermHo(Node n,
- std::set<Node>& added,
- bool withinQuant,
- bool withinInstClosure)
+void TermDb::addTermHo(Node n)
{
Assert(options::ufHo());
if (n.getType().isFunction())
// also add standard application version
args.insert(args.begin(), curr);
Node uf_n = nm->mkNode(APPLY_UF, args);
- addTerm(uf_n, added, withinQuant, withinInstClosure);
+ addTerm(uf_n);
}
}
bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
{
- if( options::lteRestrictInstClosure() ){
- //has to be both in inst closure and in ground assertions
- if( !isInstClosure( n ) ){
- Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl;
- return false;
- }
- // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this
- if( !hasTermCurrent( n, false ) ){
- Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl;
- return false;
- }
- }
if( options::instMaxLevel()!=-1 ){
if( n.hasAttribute(InstLevelAttribute()) ){
int fml = f.isNull() ? -1 : d_quantEngine->getQuantAttributes()->getQuantInstLevel( f );
}
}
-bool TermDb::isInstClosure( Node r ) {
- return d_iclosure_processed.find( r )!=d_iclosure_processed.end();
-}
-
void TermDb::setHasTerm( Node n ) {
Trace("term-db-debug2") << "hasTerm : " << n << std::endl;
if( d_has_map.find( n )==d_has_map.end() ){
d_op_map.clear();
d_type_map.clear();
d_processed.clear();
- d_iclosure_processed.clear();
}
}
}
//compute has map
- if (options::termDbMode() == options::TermDbMode::RELEVANT
- || options::lteRestrictInstClosure())
+ if (options::termDbMode() == options::TermDbMode::RELEVANT)
{
d_has_map.clear();
d_term_elig_eqc.clear();
it != it_end;
++it)
{
- if ((*it).d_assertion.getKind() != INST_CLOSURE)
- {
- setHasTerm((*it).d_assertion);
- }
+ setHasTerm((*it).d_assertion);
}
}
}
- //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
- for (const Node& n : d_iclosure_processed)
- {
- if (!ee->hasTerm(n))
- {
- ee->addTerm(n);
- }
- }
if( options::ufHo() && options::hoMergeTermDb() ){
Trace("quant-ho") << "TermDb::reset : compute equal functions..." << std::endl;
* variable per type.
*/
Node getOrMakeTypeFreshVariable(TypeNode tn);
- /** add a term to the database
- * withinQuant is whether n is within the body of a quantified formula
- * withinInstClosure is whether n is within an inst-closure operator (see
- * Bansal et al CAV 2015).
- */
- void addTerm(Node n,
- std::set<Node>& added,
- bool withinQuant = false,
- bool withinInstClosure = false);
+ /**
+ * Add a term to the database, which registers it as a term that may be
+ * matched with via E-matching, and can be used in entailment tests below.
+ */
+ void addTerm(Node n);
/** get match operator for term n
*
* If n has a kind that we index, this function will
bool isTermEligibleForInstantiation(TNode n, TNode f);
/** get eligible term in equivalence class of r */
Node getEligibleTermInEqc(TNode r);
- /** is r a inst closure node?
- * This terminology was used for specifying
- * a particular status of nodes for
- * Bansal et al., CAV 2015.
- */
- bool isInstClosure(Node r);
/** get higher-order type match predicate
*
* This predicate is used to force certain functions f of type tn to appear as
QuantifiersInferenceManager& d_qim;
/** terms processed */
std::unordered_set< Node, NodeHashFunction > d_processed;
- /** terms processed */
- std::unordered_set< Node, NodeHashFunction > d_iclosure_processed;
/** select op map */
std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
/** whether master equality engine is UF-inconsistent */
* Above, we set d_ho_fun_op_purify[(@ f 0)] = pfun, and
* d_ho_purify_to_term[(pfun 1)] = (@ (@ f 0) 1).
*/
- void addTermHo(Node n,
- std::set<Node>& added,
- bool withinQuant,
- bool withinInstClosure);
+ void addTermHo(Node n);
/** get operator representative */
Node getOperatorRepresentative( TNode op ) const;
//------------------------------end higher-order term indexing
{
getQuantifiersEngine()->assertQuantifier(atom, polarity);
}
- else if (k == INST_CLOSURE)
- {
- if (!polarity)
- {
- Unhandled() << "Unexpected inst-closure fact " << fact;
- }
- getQuantifiersEngine()->addTermToDatabase(atom[0], false, true);
- if (!options::lteRestrictInstClosure())
- {
- d_qstate.getEqualityEngine()->addTerm(atom[0]);
- }
- }
else
{
Unhandled() << "Unexpected fact " << fact;
}
};/* struct QuantifierInstPatternListTypeRule */
-struct QuantifierInstClosureTypeRule {
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- Assert(n.getKind() == kind::INST_CLOSURE);
- if( check ){
- TypeNode tn = n[0].getType(check);
- if( tn.isBoolean() ){
- throw TypeCheckingExceptionPrivate(n, "argument of inst-closure must be non-boolean");
- }
- }
- return nodeManager->booleanType();
- }
-};/* struct QuantifierInstClosureTypeRule */
-
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
d_ierCounter_c(qstate.getSatContext()),
d_presolve(qstate.getUserContext(), true),
d_presolve_in(qstate.getUserContext()),
- d_presolve_cache(qstate.getUserContext()),
- d_presolve_cache_wq(qstate.getUserContext()),
- d_presolve_cache_wic(qstate.getUserContext())
+ d_presolve_cache(qstate.getUserContext())
{
//---- utilities
// term util must come before the other utilities
//add all terms to database
if( options::incrementalSolving() ){
Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache.size() << std::endl;
- for( unsigned i=0; i<d_presolve_cache.size(); i++ ){
- addTermToDatabase( d_presolve_cache[i], d_presolve_cache_wq[i], d_presolve_cache_wic[i] );
+ for (const Node& t : d_presolve_cache)
+ {
+ addTermToDatabase(t);
}
Trace("quant-engine-proc") << "Done add presolve cache " << std::endl;
}
addTermToDatabase(d_term_util->getInstConstantBody(f), true);
}
-void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
+void QuantifiersEngine::addTermToDatabase(Node n, bool withinQuant)
+{
+ // don't add terms in quantifier bodies
+ if (withinQuant && !options::registerQuantBodyTerms())
+ {
+ return;
+ }
if( options::incrementalSolving() ){
if( d_presolve_in.find( n )==d_presolve_in.end() ){
d_presolve_in.insert( n );
d_presolve_cache.push_back( n );
- d_presolve_cache_wq.push_back( withinQuant );
- d_presolve_cache_wic.push_back( withinInstClosure );
}
}
//only wait if we are doing incremental solving
if( !d_presolve || !options::incrementalSolving() ){
- std::set< Node > added;
- d_term_db->addTerm(n, added, withinQuant, withinInstClosure);
-
- if (!withinQuant)
+ d_term_db->addTerm(n);
+ if (d_sygus_tdb && options::sygusEvalUnfold())
{
- if (d_sygus_tdb && options::sygusEvalUnfold())
- {
- d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
- }
+ d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
}
}
}
public:
/** add term to database */
- void addTermToDatabase(Node n,
- bool withinQuant = false,
- bool withinInstClosure = false);
+ void addTermToDatabase(Node n, bool withinQuant = false);
/** notification when master equality engine is updated */
void eqNotifyNewClass(TNode t);
/** debug print equality engine */
/** presolve cache */
NodeSet d_presolve_in;
NodeList d_presolve_cache;
- BoolList d_presolve_cache_wq;
- BoolList d_presolve_cache_wic;
};/* class QuantifiersEngine */
}/* CVC4::theory namespace */
projects / cvc5.git / commitdiff