From 42f51547174e2644a244464c170115ff3b2bc22f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 23 Dec 2020 15:26:24 -0600 Subject: [PATCH] Remove quant EPR option (#5716) This was an experimental option used in combination with separation logic. --- src/CMakeLists.txt | 4 - src/options/quantifiers_options.toml | 19 -- src/smt/set_defaults.cpp | 13 -- .../cegqi/ceg_epr_instantiator.cpp | 180 ----------------- .../quantifiers/cegqi/ceg_epr_instantiator.h | 109 ---------- .../quantifiers/cegqi/ceg_instantiator.cpp | 28 --- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 28 --- src/theory/quantifiers/quant_epr.cpp | 187 ------------------ src/theory/quantifiers/quant_epr.h | 104 ---------- src/theory/quantifiers_engine.cpp | 11 +- src/theory/quantifiers_engine.h | 5 - src/theory/sep/theory_sep.cpp | 57 +----- src/theory/sep/theory_sep.h | 1 - test/regress/CMakeLists.txt | 7 +- 14 files changed, 9 insertions(+), 744 deletions(-) delete mode 100644 src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp delete mode 100644 src/theory/quantifiers/cegqi/ceg_epr_instantiator.h delete mode 100644 src/theory/quantifiers/quant_epr.cpp delete mode 100644 src/theory/quantifiers/quant_epr.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 152d2e4ff..08404ce73 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -630,8 +630,6 @@ libcvc4_add_sources( theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h theory/quantifiers/cegqi/ceg_dt_instantiator.cpp theory/quantifiers/cegqi/ceg_dt_instantiator.h - theory/quantifiers/cegqi/ceg_epr_instantiator.cpp - theory/quantifiers/cegqi/ceg_epr_instantiator.h theory/quantifiers/cegqi/ceg_instantiator.cpp theory/quantifiers/cegqi/ceg_instantiator.h theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -696,8 +694,6 @@ libcvc4_add_sources( theory/quantifiers/proof_checker.h theory/quantifiers/quant_conflict_find.cpp theory/quantifiers/quant_conflict_find.h - theory/quantifiers/quant_epr.cpp - theory/quantifiers/quant_epr.h theory/quantifiers/quant_relevance.cpp theory/quantifiers/quant_relevance.h theory/quantifiers/quant_rep_bound_ext.cpp diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 4aa612d5b..9027e7a94 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1702,25 +1702,6 @@ header = "options/quantifiers_options.h" read_only = true help = "non-optimal bounds for counterexample-based quantifier instantiation" -# CEGQI for EPR - -[[option]] - name = "quantEpr" - category = "regular" - long = "quant-epr" - type = "bool" - default = "false" - help = "infer whether in effectively propositional fragment, use for cegqi" - -[[option]] - name = "quantEprMatching" - category = "regular" - long = "quant-epr-match" - type = "bool" - default = "true" - read_only = true - help = "use matching heuristics for EPR instantiation" - # CEGQI for BV [[option]] diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 8b0986db6..a781bc44b 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -811,7 +811,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // disable modes not supported by incremental options::sortInference.set(false); options::ufssFairnessMonotone.set(false); - options::quantEpr.set(false); options::globalNegate.set(false); options::bvAbstraction.set(false); options::arithMLTrick.set(false); @@ -904,18 +903,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) options::finiteModelFind.set(true); } } - // EPR - if (options::quantEpr()) - { - if (!options::preSkolemQuant.wasSetByUser()) - { - options::preSkolemQuant.set(true); - } - // must have separation logic - logic = logic.getUnlockedCopy(); - logic.enableTheory(THEORY_SEP); - logic.lock(); - } // now, have determined whether finite model find is on/off // apply finite model finding options diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp deleted file mode 100644 index 3a7e03c12..000000000 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp +++ /dev/null @@ -1,180 +0,0 @@ -/********************* */ -/*! \file ceg_epr_instantiator.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of ceg_epr_instantiator - **/ - -#include "theory/quantifiers/cegqi/ceg_epr_instantiator.h" - -#include "expr/node_algorithm.h" -#include "options/quantifiers_options.h" -#include "theory/quantifiers/ematching/trigger.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers_engine.h" - -using namespace std; -using namespace CVC4::kind; -using namespace CVC4::context; - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -void EprInstantiator::reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) -{ - d_equal_terms.clear(); -} - -bool EprInstantiator::hasProcessEqualTerm(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) -{ - return true; -} - -bool EprInstantiator::processEqualTerm(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - TermProperties& pv_prop, - Node n, - CegInstEffort effort) -{ - if (options::quantEprMatching()) - { - Assert(pv_prop.isBasic()); - d_equal_terms.push_back(n); - return false; - } - pv_prop.d_type = CEG_TT_EQUAL; - return ci->constructInstantiationInc(pv, n, pv_prop, sf); -} - -struct sortEqTermsMatch -{ - std::map d_match_score; - bool operator()(Node i, Node j) - { - int match_score_i = d_match_score[i]; - int match_score_j = d_match_score[j]; - return match_score_i > match_score_j - || (match_score_i == match_score_j && i < j); - } -}; - -bool EprInstantiator::processEqualTerms(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - std::vector& eqc, - CegInstEffort effort) -{ - if (!options::quantEprMatching()) - { - return false; - } - // heuristic for best matching constant - sortEqTermsMatch setm; - for (unsigned i = 0; i < ci->getNumCEAtoms(); i++) - { - Node catom = ci->getCEAtom(i); - computeMatchScore(ci, pv, catom, catom, setm.d_match_score); - } - // sort by match score - std::sort(d_equal_terms.begin(), d_equal_terms.end(), setm); - TermProperties pv_prop; - pv_prop.d_type = CEG_TT_EQUAL; - for (unsigned i = 0, size = d_equal_terms.size(); i < size; i++) - { - if (ci->constructInstantiationInc(pv, d_equal_terms[i], pv_prop, sf)) - { - return true; - } - } - return false; -} - -void EprInstantiator::computeMatchScore(CegInstantiator* ci, - Node pv, - Node catom, - std::vector& arg_reps, - TNodeTrie* tat, - unsigned index, - std::map& match_score) -{ - if (index == catom.getNumChildren()) - { - Assert(tat->hasData()); - Node gcatom = tat->getData(); - Trace("cegqi-epr") << "Matched : " << catom << " and " << gcatom - << std::endl; - for (unsigned i = 0, nchild = catom.getNumChildren(); i < nchild; i++) - { - if (catom[i] == pv) - { - Trace("cegqi-epr") << "...increment " << gcatom[i] << std::endl; - match_score[gcatom[i]]++; - } - else - { - // recursive matching - computeMatchScore(ci, pv, catom[i], gcatom[i], match_score); - } - } - return; - } - std::map::iterator it = tat->d_data.find(arg_reps[index]); - if (it != tat->d_data.end()) - { - computeMatchScore( - ci, pv, catom, arg_reps, &it->second, index + 1, match_score); - } -} - -void EprInstantiator::computeMatchScore(CegInstantiator* ci, - Node pv, - Node catom, - Node eqc, - std::map& match_score) -{ - if (!inst::Trigger::isAtomicTrigger(catom) || !expr::hasSubterm(catom, pv)) - { - return; - } - Trace("cegqi-epr") << "Find matches for " << catom << "..." << std::endl; - eq::EqualityEngine* ee = - ci->getQuantifiersEngine()->getMasterEqualityEngine(); - std::vector arg_reps; - for (unsigned j = 0, nchild = catom.getNumChildren(); j < nchild; j++) - { - arg_reps.push_back(ee->getRepresentative(catom[j])); - } - if (!ee->hasTerm(eqc)) - { - return; - } - TermDb* tdb = ci->getQuantifiersEngine()->getTermDatabase(); - Node rep = ee->getRepresentative(eqc); - Node op = tdb->getMatchOperator(catom); - TNodeTrie* tat = tdb->getTermArgTrie(rep, op); - Trace("cegqi-epr") << "EPR instantiation match term : " << catom - << ", check ground terms=" << (tat != NULL) << std::endl; - if (tat) - { - computeMatchScore(ci, pv, catom, arg_reps, tat, 0, match_score); - } -} - -} // namespace quantifiers -} // namespace theory -} // namespace CVC4 diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h deleted file mode 100644 index 7b46d8a45..000000000 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h +++ /dev/null @@ -1,109 +0,0 @@ -/********************* */ -/*! \file ceg_epr_instantiator.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief ceg_epr_instantiator - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H -#define CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H - -#include -#include -#include "expr/node_trie.h" -#include "theory/quantifiers/cegqi/ceg_instantiator.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -/** Effectively Propositional (EPR) Instantiator - * - * This implements a selection function for the EPR fragment. - */ -class EprInstantiator : public Instantiator -{ - public: - EprInstantiator(TypeNode tn) : Instantiator(tn) {} - virtual ~EprInstantiator() {} - /** reset */ - void reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - /** this instantiator implements hasProcessEqualTerm */ - bool hasProcessEqualTerm(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - /** process equal terms - * - * This adds n to the set of equal terms d_equal_terms if matching heuristics - * are enabled (--quant-epr-match), or simply tries the substitution pv -> n - * otherwise. - */ - bool processEqualTerm(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - TermProperties& pv_prop, - Node n, - CegInstEffort effort) override; - /** process equal terms - * - * Called when pv is equal to the set eqc. If matching heuristics are enabled, - * this adds the substitution pv -> n based on the best term n in eqc. - */ - bool processEqualTerms(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - std::vector& eqc, - CegInstEffort effort) override; - /** identify */ - std::string identify() const override { return "Epr"; } - - private: - /** - * The current set of terms that are equal to the variable-to-instantate of - * this class. - */ - std::vector d_equal_terms; - /** compute match score - * - * This method computes the map match_score, from ground term t to the - * number of times that occur in simple matches for a quantified formula. - * For example, for quantified formula forall xy. P( x ) V Q( x, y ) and - * ground terms { P( a ), Q( a, a ), Q( b, c ), Q( a, c ) }, we compute for x: - * match_score[a] = 3, - * match_score[b] = 1, - * match_score[c] = 0. - * The higher the match score for a term, the more likely this class is to use - * t in instantiations. - */ - void computeMatchScore(CegInstantiator* ci, - Node pv, - Node catom, - std::vector& arg_reps, - TNodeTrie* tat, - unsigned index, - std::map& match_score); - void computeMatchScore(CegInstantiator* ci, - Node pv, - Node catom, - Node eqc, - std::map& match_score); -}; - -} // namespace quantifiers -} // namespace theory -} // namespace CVC4 - -#endif /* CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 561450dc9..a8632c02f 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -17,14 +17,12 @@ #include "theory/quantifiers/cegqi/ceg_arith_instantiator.h" #include "theory/quantifiers/cegqi/ceg_bv_instantiator.h" #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h" -#include "theory/quantifiers/cegqi/ceg_epr_instantiator.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" @@ -372,17 +370,6 @@ CegHandledStatus CegInstantiator::isCbqiSort( } } } - else if (tn.isSort()) - { - QuantEPR* qepr = qe != nullptr ? qe->getQuantEPR() : nullptr; - if (qepr != nullptr) - { - if (qepr->isEPR(tn)) - { - ret = CEG_HANDLED_UNCONDITIONAL; - } - } - } // sets, arrays, functions and others are not supported visited[tn] = ret; return ret; @@ -489,8 +476,6 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index) Instantiator * vinst; if( tn.isReal() ){ vinst = new ArithInstantiator(tn, d_parent->getVtsTermCache()); - }else if( tn.isSort() ){ - vinst = new EprInstantiator(tn); }else if( tn.isDatatype() ){ vinst = new DtInstantiator(tn); }else if( tn.isBitVector() ){ @@ -1113,19 +1098,6 @@ bool CegInstantiator::isEligibleForInstantiation(Node n) const // virtual terms are allowed return true; } - TypeNode tn = n.getType(); - if (tn.isSort()) - { - QuantEPR* qepr = d_qe->getQuantEPR(); - if (qepr != NULL) - { - // legal if in the finite set of constants of type tn - if (qepr->isEPRConstant(tn, n)) - { - return true; - } - } - } // only legal if current quantified formula contains n return expr::hasSubterm(d_quant, n); } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index db76efd9d..16c7476ab 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -21,7 +21,6 @@ #include "theory/arith/theory_arith_private.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" @@ -115,33 +114,6 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl; registerCounterexampleLemma( q, lem ); - //totality lemmas for EPR - QuantEPR * qepr = d_quantEngine->getQuantEPR(); - if( qepr!=NULL ){ - for( unsigned i=0; iisEPR( tn ) ){ - //add totality lemma - std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn ); - if( itc!=qepr->d_consts.end() ){ - Assert(!itc->second.empty()); - Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ); - std::vector< Node > disj; - for( unsigned j=0; jsecond.size(); j++ ){ - disj.push_back( ic.eqNode( itc->second[j] ) ); - } - Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ); - Trace("cegqi-lemma") << "EPR totality lemma : " << tlem << std::endl; - d_quantEngine->getOutputChannel().lemma( tlem ); - }else{ - Assert(false); - } - } - } - } - } - //compute dependencies between quantified formulas std::vector ics; TermUtil::computeInstConstContains(q, ics); diff --git a/src/theory/quantifiers/quant_epr.cpp b/src/theory/quantifiers/quant_epr.cpp deleted file mode 100644 index cf2deee11..000000000 --- a/src/theory/quantifiers/quant_epr.cpp +++ /dev/null @@ -1,187 +0,0 @@ -/********************* */ -/*! \file quant_epr.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of quantifier EPR. - **/ - -#include "theory/quantifiers/quant_epr.h" - -#include "theory/quantifiers/quant_util.h" - -using namespace CVC4::kind; - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -void QuantEPR::registerNode(Node n, - std::map >& visited, - bool beneathQuant, - bool hasPol, - bool pol) -{ - int vindex = hasPol ? (pol ? 1 : -1) : 0; - if (visited[vindex].find(n) == visited[vindex].end()) - { - visited[vindex][n] = true; - Trace("quant-epr-debug") << "QuantEPR::registerNode " << n << std::endl; - if (n.getKind() == FORALL) - { - if (beneathQuant || !hasPol || !pol) - { - for (unsigned i = 0; i < n[0].getNumChildren(); i++) - { - TypeNode tn = n[0][i].getType(); - if (d_non_epr.find(tn) == d_non_epr.end()) - { - Trace("quant-epr") << "Sort " << tn - << " is non-EPR because of nested or possible " - "existential quantification." - << std::endl; - d_non_epr[tn] = true; - } - } - } - else - { - beneathQuant = true; - } - } - TypeNode tn = n.getType(); - - if (n.getNumChildren() > 0) - { - if (tn.isSort()) - { - if (d_non_epr.find(tn) == d_non_epr.end()) - { - Trace("quant-epr") << "Sort " << tn << " is non-EPR because of " << n - << std::endl; - d_non_epr[tn] = true; - } - } - for (unsigned i = 0; i < n.getNumChildren(); i++) - { - bool newHasPol; - bool newPol; - QuantPhaseReq::getPolarity(n, i, hasPol, pol, newHasPol, newPol); - registerNode(n[i], visited, beneathQuant, newHasPol, newPol); - } - } - else if (tn.isSort()) - { - if (n.getKind() == BOUND_VARIABLE) - { - if (d_consts.find(tn) == d_consts.end()) - { - // mark that at least one constant must occur - d_consts[tn].clear(); - } - } - else if (std::find(d_consts[tn].begin(), d_consts[tn].end(), n) - == d_consts[tn].end()) - { - d_consts[tn].push_back(n); - Trace("quant-epr") << "...constant of type " << tn << " : " << n - << std::endl; - } - } - } -} - -void QuantEPR::registerAssertion(Node assertion) -{ - std::map > visited; - registerNode(assertion, visited, false, true, true); -} - -void QuantEPR::finishInit() -{ - Trace("quant-epr-debug") << "QuantEPR::finishInit" << std::endl; - for (std::map >::iterator it = d_consts.begin(); - it != d_consts.end(); - ++it) - { - Assert(d_epr_axiom.find(it->first) == d_epr_axiom.end()); - Trace("quant-epr-debug") << "process " << it->first << std::endl; - if (d_non_epr.find(it->first) != d_non_epr.end()) - { - Trace("quant-epr-debug") << "...non-epr" << std::endl; - it->second.clear(); - } - else - { - Trace("quant-epr-debug") << "...epr, #consts = " << it->second.size() - << std::endl; - if (it->second.empty()) - { - it->second.push_back(NodeManager::currentNM()->mkSkolem( - "e", it->first, "EPR base constant")); - } - if (Trace.isOn("quant-epr")) - { - Trace("quant-epr") << "Type " << it->first - << " is EPR, with constants : " << std::endl; - for (unsigned i = 0; i < it->second.size(); i++) - { - Trace("quant-epr") << " " << it->second[i] << std::endl; - } - } - } - } -} - -bool QuantEPR::isEPRConstant(TypeNode tn, Node k) -{ - return std::find(d_consts[tn].begin(), d_consts[tn].end(), k) - != d_consts[tn].end(); -} - -void QuantEPR::addEPRConstant(TypeNode tn, Node k) -{ - Assert(isEPR(tn)); - Assert(d_epr_axiom.find(tn) == d_epr_axiom.end()); - if (!isEPRConstant(tn, k)) - { - d_consts[tn].push_back(k); - } -} - -Node QuantEPR::mkEPRAxiom(TypeNode tn) -{ - Assert(isEPR(tn)); - std::map::iterator ita = d_epr_axiom.find(tn); - if (ita == d_epr_axiom.end()) - { - std::vector disj; - Node x = NodeManager::currentNM()->mkBoundVar(tn); - for (unsigned i = 0; i < d_consts[tn].size(); i++) - { - disj.push_back( - NodeManager::currentNM()->mkNode(EQUAL, x, d_consts[tn][i])); - } - Assert(!disj.empty()); - d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( - FORALL, - NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, x), - disj.size() == 1 ? disj[0] - : NodeManager::currentNM()->mkNode(OR, disj)); - return d_epr_axiom[tn]; - } - else - { - return ita->second; - } -} - -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/quant_epr.h b/src/theory/quantifiers/quant_epr.h deleted file mode 100644 index 752b80d6c..000000000 --- a/src/theory/quantifiers/quant_epr.h +++ /dev/null @@ -1,104 +0,0 @@ -/********************* */ -/*! \file quant_epr.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief quantifier util - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__THEORY__QUANT_EPR_H -#define CVC4__THEORY__QUANT_EPR_H - -#include - -#include "expr/node.h" -#include "expr/type_node.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -/** Quant EPR - * - * This class maintains information required for - * approaches for effectively propositional logic (EPR), - * also called the Bernays-Schoenfinkel fragment. - * - * It maintains for each type whether the type - * has a finite Herbrand universe, stored in d_consts. - * This class is used in counterexample-guided instantiation - * for EPR, described in Reynolds et al., - * "Reasoning in the Bernays-Schonfinkel-Ramsey Fragment of - * Separation Logic", VMCAI 2017. - * - * Below, we say a type is an "EPR type" if its - * Herbrand universe can be restricted to a finite set - * based on the set of input assertions, - * and a "non-EPR type" otherwise. - */ -class QuantEPR -{ - public: - QuantEPR() {} - virtual ~QuantEPR() {} - /** constants per type */ - std::map > d_consts; - /** register an input assertion with this class - * This updates whether types are EPR are not - * based on the constraints in assertion. - */ - void registerAssertion(Node assertion); - /** finish initialize - * This ensures all EPR sorts are non-empty - * (that is, they have at least one term in d_consts), - * and clears non-EPR sorts from d_consts. - */ - void finishInit(); - /** is type tn an EPR type? */ - bool isEPR(TypeNode tn) const - { - return d_non_epr.find(tn) == d_non_epr.end(); - } - /** is k an EPR constant for type tn? */ - bool isEPRConstant(TypeNode tn, Node k); - /** add EPR constant k of type tn. */ - void addEPRConstant(TypeNode tn, Node k); - /** get EPR axiom for type - * This is a formula of the form: - * forall x : U. ( x = c1 V ... x = cn ) - * where c1...cn are the constants in the Herbrand - * universe of U. - */ - Node mkEPRAxiom(TypeNode tn); - /** does this class have an EPR axiom for type tn? */ - bool hasEPRAxiom(TypeNode tn) const - { - return d_epr_axiom.find(tn) != d_epr_axiom.end(); - } - - private: - /** register the node */ - void registerNode(Node n, - std::map >& visited, - bool beneathQuant, - bool hasPol, - bool pol); - /** map from types to a flag says whether they are not EPR */ - std::map d_non_epr; - /** EPR axioms for each type. */ - std::map d_epr_axiom; -}; - -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ - -#endif /* CVC4__THEORY__QUANT_EPR_H */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 3e625218c..8b3ea8622 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -43,7 +43,6 @@ QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, d_tr_trie(new inst::TriggerTrie), d_model(nullptr), d_builder(nullptr), - d_qepr(nullptr), d_term_util(new quantifiers::TermUtil(this)), d_term_canon(new expr::TermCanonize), d_term_db(new quantifiers::TermDb(d_context, d_userContext, this)), @@ -86,10 +85,6 @@ QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; - if( options::quantEpr() ){ - Assert(!options::incrementalSolving()); - d_qepr.reset(new quantifiers::QuantEPR); - } //---- end utilities //allow theory combination to go first, once initially @@ -183,10 +178,6 @@ quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const { return d_builder.get(); } -quantifiers::QuantEPR* QuantifiersEngine::getQuantEPR() const -{ - return d_qepr.get(); -} quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const { return d_model.get(); @@ -357,7 +348,7 @@ void QuantifiersEngine::ppNotifyAssertions( const std::vector& assertions) { Trace("quant-engine-proc") << "ppNotifyAssertions in QE, #assertions = " << assertions.size() - << " check epr = " << (d_qepr != NULL) << std::endl; + << std::endl; if (options::instLevelInputOnly() && options::instMaxLevel() != -1) { for (const Node& a : assertions) diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 5af914a9f..0c3bb181e 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -29,7 +29,6 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/skolemize.h" @@ -88,8 +87,6 @@ class QuantifiersEngine { EqualityQuery* getEqualityQuery() const; /** get the model builder */ quantifiers::QModelBuilder* getModelBuilder() const; - /** get utility for EPR */ - quantifiers::QuantEPR* getQuantEPR() const; /** get model */ quantifiers::FirstOrderModel* getModel() const; /** get term database */ @@ -355,8 +352,6 @@ public: std::unique_ptr d_model; /** model builder */ std::unique_ptr d_builder; - /** utility for effectively propositional logic */ - std::unique_ptr d_qepr; /** term utilities */ std::unique_ptr d_term_util; /** term utilities */ diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index d9d9415fc..299ef7239 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -24,7 +24,6 @@ #include "options/sep_options.h" #include "options/smt_options.h" #include "smt/logic_exception.h" -#include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -990,22 +989,6 @@ void TheorySep::ppNotifyAssertions(const std::vector& assertions) { d_loc_to_data_type[d_type_ref] = d_type_data; } } - // initialize the EPR utility - QuantifiersEngine* qe = getQuantifiersEngine(); - if (qe != nullptr) - { - quantifiers::QuantEPR* qepr = qe->getQuantEPR(); - if (qepr != nullptr) - { - for (const Node& a : assertions) - { - qepr->registerAssertion(a); - } - // must handle sources of other new constants e.g. separation logic - initializeBounds(); - qepr->finishInit(); - } - } } //return cardinality @@ -1030,13 +1013,10 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& if( quantifiers::TermUtil::hasBoundVarAttr( n[0] ) ){ TypeNode tn1 = n[0].getType(); if( d_bound_kind[tn1]!=bound_strict && d_bound_kind[tn1]!=bound_invalid ){ - if( options::quantEpr() && n[0].getKind()==kind::BOUND_VARIABLE ){ - // still valid : bound on heap models will include Herbrand universe of n[0].getType() - d_bound_kind[tn1] = bound_herbrand; - }else{ - d_bound_kind[tn1] = bound_invalid; - Trace("sep-bound") << "reference cannot be bound (due to quantified pto)." << std::endl; - } + d_bound_kind[tn1] = bound_invalid; + Trace("sep-bound") + << "reference cannot be bound (due to quantified pto)." + << std::endl; } }else{ references[index][n].push_back( n[0] ); @@ -1204,24 +1184,6 @@ void TheorySep::initializeBounds() { for( std::map< TypeNode, TypeNode >::iterator it = d_loc_to_data_type.begin(); it != d_loc_to_data_type.end(); ++it ){ TypeNode tn = it->first; Trace("sep-bound") << "Initialize bounds for " << tn << "..." << std::endl; - quantifiers::QuantEPR* qepr = getLogicInfo().isQuantified() - ? getQuantifiersEngine()->getQuantEPR() - : NULL; - //if pto had free variable reference - if( d_bound_kind[tn]==bound_herbrand ){ - //include Herbrand universe of tn - if( qepr && qepr->isEPR( tn ) ){ - for( unsigned j=0; jd_consts[tn].size(); j++ ){ - Node k = qepr->d_consts[tn][j]; - if( std::find( d_type_references[tn].begin(), d_type_references[tn].end(), k )==d_type_references[tn].end() ){ - d_type_references[tn].push_back( k ); - } - } - }else{ - d_bound_kind[tn] = bound_invalid; - Trace("sep-bound") << "reference cannot be bound (due to non-EPR variable)." << std::endl; - } - } unsigned n_emp = 0; if( d_bound_kind[tn] != bound_invalid ){ n_emp = d_card_max[tn]; @@ -1236,18 +1198,7 @@ void TheorySep::initializeBounds() { Node e = NodeManager::currentNM()->mkSkolem( "e", tn, "cardinality bound element for seplog" ); d_type_references_card[tn].push_back( e ); d_type_ref_card_id[e] = r; - //must include this constant back into EPR handling - if( qepr && qepr->isEPR( tn ) ){ - qepr->addEPRConstant( tn, e ); - } } - //EPR must include nil ref - if( qepr && qepr->isEPR( tn ) ){ - Node nr = getNilRef( tn ); - if( !qepr->isEPRConstant( tn, nr ) ){ - qepr->addEPRConstant( tn, nr ); - } - } } } } diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 9e96dccc3..9396200c9 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -253,7 +253,6 @@ class TheorySep : public Theory { enum { bound_strict, bound_default, - bound_herbrand, bound_invalid, }; std::map< TypeNode, unsigned > d_bound_kind; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2a3cfd9ea..62978220a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1835,8 +1835,6 @@ set(regress_1_tests regress1/sep/chain-int.smt2 regress1/sep/crash1220.smt2 regress1/sep/dispose-list-4-init.smt2 - regress1/sep/emp2-quant-unsat.smt2 - regress1/sep/finite-witness-sat.smt2 regress1/sep/fmf-nemp-2.smt2 regress1/sep/loop-1220.smt2 regress1/sep/pto-04.smt2 @@ -1844,7 +1842,6 @@ set(regress_1_tests regress1/sep/sep-02.smt2 regress1/sep/sep-03.smt2 regress1/sep/sep-find2.smt2 - regress1/sep/sep-fmf-priority.smt2 regress1/sep/sep-neg-1refine.smt2 regress1/sep/sep-neg-nstrict.smt2 regress1/sep/sep-neg-nstrict2.smt2 @@ -2480,6 +2477,10 @@ set(regression_disabled_tests regress1/rels/garbage_collect.cvc regress1/sets/setofsets-disequal.smt2 regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 + # no longer support quant-epr + sep + regress1/sep/emp2-quant-unsat.smt2 + regress1/sep/finite-witness-sat.smt2 + regress1/sep/sep-fmf-priority.smt2 regress1/simple-rdl-definefun.smt2 # does not solve after minor modification to search regress1/sygus/car_3.lus.sy -- 2.30.2