This was an experimental option used in combination with separation logic.
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
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
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]]
// 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);
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
+++ /dev/null
-/********************* */
-/*! \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<Node, int> 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<Node>& 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<Node>& arg_reps,
- TNodeTrie* tat,
- unsigned index,
- std::map<Node, int>& 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<TNode, TNodeTrie>::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<Node, int>& 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<Node> 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
+++ /dev/null
-/********************* */
-/*! \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 <map>
-#include <vector>
-#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<Node>& 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<Node> 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<Node>& arg_reps,
- TNodeTrie* tat,
- unsigned index,
- std::map<Node, int>& match_score);
- void computeMatchScore(CegInstantiator* ci,
- Node pv,
- Node catom,
- Node eqc,
- std::map<Node, int>& match_score);
-};
-
-} // namespace quantifiers
-} // namespace theory
-} // namespace CVC4
-
-#endif /* CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H */
#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"
}
}
}
- 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;
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() ){
// 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);
}
#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"
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; i<q[0].getNumChildren(); i++ ){
- TypeNode tn = q[0][i].getType();
- if( tn.isSort() ){
- if( qepr->isEPR( 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; j<itc->second.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<Node> ics;
TermUtil::computeInstConstContains(q, ics);
+++ /dev/null
-/********************* */
-/*! \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<int, std::map<Node, bool> >& 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<int, std::map<Node, bool> > visited;
- registerNode(assertion, visited, false, true, true);
-}
-
-void QuantEPR::finishInit()
-{
- Trace("quant-epr-debug") << "QuantEPR::finishInit" << std::endl;
- for (std::map<TypeNode, std::vector<Node> >::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<TypeNode, Node>::iterator ita = d_epr_axiom.find(tn);
- if (ita == d_epr_axiom.end())
- {
- std::vector<Node> 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 */
+++ /dev/null
-/********************* */
-/*! \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 <map>
-
-#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<TypeNode, std::vector<Node> > 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<int, std::map<Node, bool> >& visited,
- bool beneathQuant,
- bool hasPol,
- bool pol);
- /** map from types to a flag says whether they are not EPR */
- std::map<TypeNode, bool> d_non_epr;
- /** EPR axioms for each type. */
- std::map<TypeNode, Node> d_epr_axiom;
-};
-
-} /* CVC4::theory::quantifiers namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
-
-#endif /* CVC4__THEORY__QUANT_EPR_H */
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)),
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
{
return d_builder.get();
}
-quantifiers::QuantEPR* QuantifiersEngine::getQuantEPR() const
-{
- return d_qepr.get();
-}
quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
{
return d_model.get();
const std::vector<Node>& 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)
#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"
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 */
std::unique_ptr<quantifiers::FirstOrderModel> d_model;
/** model builder */
std::unique_ptr<quantifiers::QModelBuilder> d_builder;
- /** utility for effectively propositional logic */
- std::unique_ptr<quantifiers::QuantEPR> d_qepr;
/** term utilities */
std::unique_ptr<quantifiers::TermUtil> d_term_util;
/** term utilities */
#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"
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
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] );
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; j<qepr->d_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];
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 );
- }
- }
}
}
}
enum {
bound_strict,
bound_default,
- bound_herbrand,
bound_invalid,
};
std::map< TypeNode, unsigned > d_bound_kind;
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
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
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
projects / cvc5.git / commitdiff