namespace theory {
namespace quantifiers {
-ArithInstantiator::ArithInstantiator(QuantifiersEngine* qe, TypeNode tn)
- : Instantiator(qe, tn)
+ArithInstantiator::ArithInstantiator(TypeNode tn) : Instantiator(tn)
{
d_zero = NodeManager::currentNM()->mkConst(Rational(0));
d_one = NodeManager::currentNM()->mkConst(Rational(1));
<< pvmod << " -> " << uval << ", styp = " << uires << std::endl;
}
// take into account delta
- if (ci->useVtsDelta() && (uires == 2 || uires == -2))
+ if (uires == 2 || uires == -2)
{
if (options::cbqiModel())
{
return false;
}
NodeManager* nm = NodeManager::currentNM();
- bool use_inf = ci->useVtsInfinity()
- && (d_type.isInteger() ? options::cbqiUseInfInt()
- : options::cbqiUseInfReal());
+ bool use_inf =
+ d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal();
bool upper_first = Random::getRandom().pickWithProb(0.5);
if (options::cbqiMinBounds())
{
// if using cbqiMidpoint, only add the instance based on one bound if
// the bound is non-strict
if (!options::cbqiMidpoint() || d_type.isInteger()
- || (ci->useVtsDelta() && d_mbp_vts_coeff[rr][1][best].isNull()))
+ || d_mbp_vts_coeff[rr][1][best].isNull())
{
Node val = d_mbp_bounds[rr][best];
val = getModelBasedProjectionValue(ci,
? d_zero
: (real_part.size() == 1 ? real_part[0]
: nm->mkNode(PLUS, real_part));
- Assert(ci->getOutput()->isEligibleForInstantiation(realPart));
+ Assert(ci->isEligibleForInstantiation(realPart));
// re-isolate
Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl;
veq_c = Node::null();
class ArithInstantiator : public Instantiator
{
public:
- ArithInstantiator(QuantifiersEngine* qe, TypeNode tn);
+ ArithInstantiator(TypeNode tn);
virtual ~ArithInstantiator() {}
/** reset */
void reset(CegInstantiator* ci,
CegInstantiator* d_ci;
};
-BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn)
- : Instantiator(qe, tn), d_inst_id_counter(0)
+BvInstantiator::BvInstantiator(TypeNode tn, BvInverter* inv)
+ : Instantiator(tn), d_inverter(inv), d_inst_id_counter(0)
{
- // get the global inverter utility
- // this must be global since we need to:
+ // The inverter utility d_inverter is global to all BvInstantiator classes.
+ // This must be global since we need to:
// * process Skolem functions properly across multiple variables within the
// same quantifier
// * cache Skolem variables uniformly across multiple quantified formulas
- d_inverter = qe->getBvInverter();
}
BvInstantiator::~BvInstantiator() {}
class BvInstantiator : public Instantiator
{
public:
- BvInstantiator(QuantifiersEngine* qe, TypeNode tn);
+ BvInstantiator(TypeNode tn, BvInverter* inv);
~BvInstantiator() override;
/** reset */
void reset(CegInstantiator* ci,
class DtInstantiator : public Instantiator
{
public:
- DtInstantiator(QuantifiersEngine* qe, TypeNode tn) : Instantiator(qe, tn) {}
+ DtInstantiator(TypeNode tn) : Instantiator(tn) {}
virtual ~DtInstantiator() {}
/** reset */
void reset(CegInstantiator* ci,
class EprInstantiator : public Instantiator
{
public:
- EprInstantiator(QuantifiersEngine* qe, TypeNode tn) : Instantiator(qe, tn) {}
+ EprInstantiator(TypeNode tn) : Instantiator(tn) {}
virtual ~EprInstantiator() {}
/** reset */
void reset(CegInstantiator* ci,
#include "options/quantifiers_options.h"
#include "smt/term_formula_removal.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"
d_theta.pop_back();
}
-CegInstantiator::CegInstantiator(QuantifiersEngine* qe,
- CegqiOutput* out,
- bool use_vts_delta,
- bool use_vts_inf)
- : d_qe(qe),
- d_out(out),
- d_use_vts_delta(use_vts_delta),
- d_use_vts_inf(use_vts_inf),
+CegInstantiator::CegInstantiator(Node q, InstStrategyCegqi* parent)
+ : d_quant(q),
+ d_parent(parent),
+ d_qe(parent->getQuantifiersEngine()),
d_is_nested_quant(false),
d_effort(CEG_INST_EFFORT_NONE)
{
if (d_vars_set.find(n) != d_vars_set.end())
{
d_prog_var[n].insert(n);
- }else if( !d_out->isEligibleForInstantiation( n ) ){
+ }
+ else if (!isEligibleForInstantiation(n))
+ {
d_inelig.insert(n);
return;
}
TypeNode tn = v.getType();
Instantiator * vinst;
if( tn.isReal() ){
- vinst = new ArithInstantiator( d_qe, tn );
+ vinst = new ArithInstantiator(tn);
}else if( tn.isSort() ){
Assert( options::quantEpr() );
- vinst = new EprInstantiator( d_qe, tn );
+ vinst = new EprInstantiator(tn);
}else if( tn.isDatatype() ){
- vinst = new DtInstantiator( d_qe, tn );
+ vinst = new DtInstantiator(tn);
}else if( tn.isBitVector() ){
- vinst = new BvInstantiator( d_qe, tn );
+ vinst = new BvInstantiator(tn, d_parent->getBvInverter());
}else if( tn.isBoolean() ){
- vinst = new ModelValueInstantiator( d_qe, tn );
+ vinst = new ModelValueInstantiator(tn);
}else{
//default
- vinst = new Instantiator( d_qe, tn );
+ vinst = new Instantiator(tn);
}
d_instantiator[v] = vinst;
}
}
}
Trace("cbqi-inst-debug") << "Do the instantiation...." << std::endl;
- bool ret = d_out->doAddInstantiation( subs );
+ bool ret = d_parent->doAddInstantiation(subs);
for( unsigned i=0; i<lemmas.size(); i++ ){
- d_out->addLemma( lemmas[i] );
+ d_parent->addLemma(lemmas[i]);
}
return ret;
}
+bool CegInstantiator::isEligibleForInstantiation(Node n) const
+{
+ if (n.getKind() != INST_CONSTANT && n.getKind() != SKOLEM)
+ {
+ return true;
+ }
+ if (n.getAttribute(VirtualTermSkolemAttribute()))
+ {
+ // 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);
+}
+
bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){
Assert( d_prog_var.find( n )!=d_prog_var.end() );
if( !non_basic.empty() ){
}
}
-
-Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){
+Instantiator::Instantiator(TypeNode tn) : d_type(tn)
+{
d_closed_enum_type = tn.isClosedEnumerable();
}
namespace quantifiers {
-class CegqiOutput {
-public:
- virtual ~CegqiOutput() {}
- virtual bool doAddInstantiation( std::vector< Node >& subs ) = 0;
- virtual bool isEligibleForInstantiation( Node n ) = 0;
- virtual bool addLemma( Node lem ) = 0;
-};
-
class Instantiator;
class InstantiatorPreprocess;
+class InstStrategyCegqi;
/** Term Properties
*
*/
class CegInstantiator {
public:
- CegInstantiator(QuantifiersEngine* qe,
- CegqiOutput* out,
- bool use_vts_delta = true,
- bool use_vts_inf = true);
+ /**
+ * The instantiator will be constructing instantiations for quantified formula
+ * q, parent is the owner of this object.
+ */
+ CegInstantiator(Node q, InstStrategyCegqi* parent);
virtual ~CegInstantiator();
/** check
* This adds instantiations based on the state of d_vars in current context
*/
void registerCounterexampleLemma(std::vector<Node>& lems,
std::vector<Node>& ce_vars);
- /** get the output channel of this class */
- CegqiOutput* getOutput() { return d_out; }
//------------------------------interface for instantiators
/** get quantifiers engine */
QuantifiersEngine* getQuantifiersEngine() { return d_qe; }
bool isEligible(Node n);
/** does n have variable pv? */
bool hasVariable(Node n, Node pv);
- /** are we using delta for LRA virtual term substitution? */
- bool useVtsDelta() { return d_use_vts_delta; }
- /** are we using infinity for LRA virtual term substitution? */
- bool useVtsInfinity() { return d_use_vts_inf; }
/** are we processing a nested quantified formula? */
- bool hasNestedQuantification() { return d_is_nested_quant; }
+ bool hasNestedQuantification() const { return d_is_nested_quant; }
+ /**
+ * Are we allowed to instantiate the current quantified formula with n? This
+ * includes restrictions such as if n is a variable, it must occur free in
+ * the current quantified formula.
+ */
+ bool isEligibleForInstantiation(Node n) const;
//------------------------------------ static queries
/** Is k a kind for which counterexample-guided instantiation is possible?
*
static CegHandledStatus isCbqiQuant(Node q, QuantifiersEngine* qe = nullptr);
//------------------------------------ end static queries
private:
+ /** The quantified formula of this instantiator */
+ Node d_quant;
+ /** The parent of this instantiator */
+ InstStrategyCegqi* d_parent;
/** quantified formula associated with this instantiator */
QuantifiersEngine* d_qe;
- /** output channel of this instantiator */
- CegqiOutput* d_out;
- /** whether we are using delta for virtual term substitution
- * (for quantified LRA).
- */
- bool d_use_vts_delta;
- /** whether we are using infinity for virtual term substitution
- * (for quantified LRA).
- */
- bool d_use_vts_inf;
//-------------------------------globally cached
/** cache from nodes to the set of variables it contains
*/
class Instantiator {
public:
- Instantiator( QuantifiersEngine * qe, TypeNode tn );
- virtual ~Instantiator(){}
- /** reset
- * This is called once, prior to any of the below methods are called.
- * This function sets up any initial information necessary for constructing
- * instantiations for pv based on the current context.
- */
- virtual void reset(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort)
- {
- }
+ Instantiator(TypeNode tn);
+ virtual ~Instantiator() {}
+ /** reset
+ * This is called once, prior to any of the below methods are called.
+ * This function sets up any initial information necessary for constructing
+ * instantiations for pv based on the current context.
+ */
+ virtual void reset(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort)
+ {
+ }
/** has process equal term
*
class ModelValueInstantiator : public Instantiator {
public:
- ModelValueInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
- virtual ~ModelValueInstantiator(){}
- bool useModelValue(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort) override
- {
- return true;
- }
+ ModelValueInstantiator(TypeNode tn) : Instantiator(tn) {}
+ virtual ~ModelValueInstantiator() {}
+ bool useModelValue(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override
+ {
+ return true;
+ }
std::string identify() const override { return "ModelValue"; }
};
#include "theory/theory_engine.h"
using namespace std;
-using namespace CVC4;
using namespace CVC4::kind;
using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-bool CegqiOutputInstStrategy::doAddInstantiation(std::vector<Node>& subs)
-{
- return d_out->doAddInstantiation(subs);
-}
-
-bool CegqiOutputInstStrategy::isEligibleForInstantiation(Node n)
-{
- return d_out->isEligibleForInstantiation(n);
-}
-
-bool CegqiOutputInstStrategy::addLemma(Node lem)
-{
- return d_out->addLemma(lem);
-}
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
: QuantifiersModule(qe),
d_incomplete_check(false),
d_added_cbqi_lemma(qe->getUserContext()),
d_elim_quants(qe->getSatContext()),
- d_out(new CegqiOutputInstStrategy(this)),
+ d_bv_invert(nullptr),
d_nested_qe_waitlist_size(qe->getUserContext()),
d_nested_qe_waitlist_proc(qe->getUserContext())
-//, d_added_inst( qe->getUserContext() )
{
d_qid_count = 0;
d_small_const =
NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000));
d_check_vts_lemma_lc = false;
+ if (options::cbqiBv())
+ {
+ // if doing instantiation for BV, need the inverter class
+ d_bv_invert.reset(new quantifiers::BvInverter);
+ }
}
InstStrategyCegqi::~InstStrategyCegqi() {}
return d_quantEngine->addLemma( lem );
}
-bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
- if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){
- if( n.getAttribute(VirtualTermSkolemAttribute()) ){
- // virtual terms are allowed
- return true;
- }else{
- TypeNode tn = n.getType();
- if( tn.isSort() ){
- QuantEPR * qepr = d_quantEngine->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_curr_quant, n);
- }
- }else{
- return true;
- }
-}
CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
d_cinst.find(q);
if( it==d_cinst.end() ){
- d_cinst[q].reset(
- new CegInstantiator(d_quantEngine, d_out.get(), true, true));
+ d_cinst[q].reset(new CegInstantiator(q, this));
return d_cinst[q].get();
}
return it->second.get();
}
+BvInverter* InstStrategyCegqi::getBvInverter() const
+{
+ return d_bv_invert.get();
+}
+
void InstStrategyCegqi::presolve() {
if (!options::cbqiPreRegInst())
{
}
}
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
#include "theory/decision_manager.h"
+#include "theory/quantifiers/bv_inverter.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
#include "theory/quantifiers/quant_util.h"
#include "util/statistics_registry.h"
namespace theory {
namespace quantifiers {
-class InstStrategyCegqi;
-
-/**
- * An output channel class, used by instantiator objects below. The methods
- * of this class call the corresponding functions of InstStrategyCegqi below.
- */
-class CegqiOutputInstStrategy : public CegqiOutput
-{
- public:
- CegqiOutputInstStrategy(InstStrategyCegqi* out) : d_out(out) {}
- /** The module whose functions we call. */
- InstStrategyCegqi* d_out;
- /** add instantiation */
- bool doAddInstantiation(std::vector<Node>& subs) override;
- /** is eligible for instantiation */
- bool isEligibleForInstantiation(Node n) override;
- /** add lemma */
- bool addLemma(Node lem) override;
-};
-
/**
* Counterexample-guided quantifier instantiation module.
*
std::string identify() const override { return std::string("Cegqi"); }
/** get instantiator for quantifier */
CegInstantiator* getInstantiator(Node q);
+ /** get the BV inverter utility */
+ BvInverter* getBvInverter() const;
/** pre-register quantifier */
void preRegisterQuantifier(Node q) override;
// presolve
//------------------- interface for CegqiOutputInstStrategy
/** Instantiate the current quantified formula forall x. Q with x -> subs. */
bool doAddInstantiation(std::vector<Node>& subs);
- /**
- * Are we allowed to instantiate the current quantified formula with n? This
- * includes restrictions such as if n is a variable, it must occur free in
- * the current quantified formula.
- */
- bool isEligibleForInstantiation(Node n);
/** Add lemma lem via the output channel of this class. */
bool addLemma(Node lem);
//------------------- end interface for CegqiOutputInstStrategy
std::map< Node, bool > d_active_quant;
/** Whether cegqi handles each quantified formula. */
std::map<Node, CegHandledStatus> d_do_cbqi;
- /**
- * An output channel used by instantiators for communicating with this
- * class.
- */
- std::unique_ptr<CegqiOutputInstStrategy> d_out;
/**
* The instantiator for each quantified formula q registered to this class.
* This object is responsible for finding instantiatons for q.
*/
std::map<Node, std::unique_ptr<CegInstantiator>> d_cinst;
+ /** inversion utility for BV instantiation */
+ std::unique_ptr<BvInverter> d_bv_invert;
/**
* The decision strategy for each quantified formula q registered to this
* class.
d_tr_trie(new inst::TriggerTrie),
d_model(nullptr),
d_rel_dom(nullptr),
- d_bv_invert(nullptr),
d_builder(nullptr),
d_qepr(nullptr),
d_term_util(new quantifiers::TermUtil(this)),
Assert( !options::incrementalSolving() );
d_qepr.reset(new quantifiers::QuantEPR);
}
-
- if (options::cbqi() && options::cbqiBv())
- {
- // if doing instantiation for BV, need the inverter class
- d_bv_invert.reset(new quantifiers::BvInverter);
- }
//---- end utilities
//allow theory combination to go first, once initially
{
return d_rel_dom.get();
}
-quantifiers::BvInverter* QuantifiersEngine::getBvInverter() const
-{
- return d_bv_invert.get();
-}
quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
{
return d_builder.get();
#include "context/cdlist.h"
#include "expr/attribute.h"
#include "expr/term_canonize.h"
-#include "theory/quantifiers/bv_inverter.h"
#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/equality_infer.h"
quantifiers::EqualityInference* getEqualityInference() const;
/** get relevant domain */
quantifiers::RelevantDomain* getRelevantDomain() const;
- /** get the BV inverter utility */
- quantifiers::BvInverter* getBvInverter() const;
//---------------------- end utilities
//---------------------- modules (TODO remove these #1163)
/** get bounded integers utility */
std::unique_ptr<quantifiers::FirstOrderModel> d_model;
/** relevant domain */
std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
- /** inversion utility for BV instantiation */
- std::unique_ptr<quantifiers::BvInverter> d_bv_invert;
/** model builder */
std::unique_ptr<quantifiers::QModelBuilder> d_builder;
/** utility for effectively propositional logic */
projects / cvc5.git / commitdiff