* Document TermDb and related classes. Minor changes to quantifiers utils and their interface. Address some comments left over from PR 1206.
* Minor
* Minor
* Change namespace style.
* Address review
* Fix incorrectly merged portion that led to regression failures.
* New clang format, fully document relevant domain.
* Clang format again.
* Minor
#include "theory/uf/equality_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;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){
}
}
-Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
- Assert( f.isNull() || f.getKind()==FORALL );
+Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
+ Node q,
+ int index)
+{
+ Assert(q.isNull() || q.getKind() == FORALL);
Node r = getRepresentative( a );
if( options::finiteModelFind() ){
if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){
if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){
return r;
}else{
- TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType();
- std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r );
- if( itir==d_int_rep[v_tn].end() ){
+ TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType();
+ std::map<Node, Node>& v_int_rep = d_int_rep[v_tn];
+ std::map<Node, Node>::const_iterator itir = v_int_rep.find(r);
+ if (itir != v_int_rep.end())
+ {
+ return itir->second;
+ }
+ else
+ {
//find best selection for representative
Node r_best;
- //if( options::fmfRelevantDomain() && !f.isNull() ){
- // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
- // r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r );
- // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
+ // if( options::fmfRelevantDomain() && !q.isNull() ){
+ // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " <<
+ // r << std::endl;
+ // r_best = d_qe->getRelevantDomain()->getRelevantTerm( q, index, r );
+ // Trace("internal-rep-debug") << "Returned " << r_best << " " << r <<
+ // std::endl;
//}
std::vector< Node > eqc;
getEquivalenceClass( r, eqc );
Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
for( unsigned i=0; i<eqc.size(); i++ ){
- if( i>0 ) Trace("internal-rep-select") << ", ";
+ if (i > 0)
+ {
+ Trace("internal-rep-select") << ", ";
+ }
Trace("internal-rep-select") << eqc[i];
}
Trace("internal-rep-select") << " }, type = " << v_tn << std::endl;
int r_best_score = -1;
for( size_t i=0; i<eqc.size(); i++ ){
- int score = getRepScore( eqc[i], f, index, v_tn );
+ int score = getRepScore(eqc[i], q, index, v_tn);
if( score!=-2 ){
if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
r_best = eqc[i];
}
Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl;
Assert( r_best.getType().isSubtypeOf( v_tn ) );
- d_int_rep[v_tn][r] = r_best;
+ v_int_rep[r] = r_best;
if( r_best!=a ){
Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
}
return r_best;
- }else{
- return itir->second;
}
}
}
}
//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
-int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){
+int EqualityQueryQuantifiersEngine::getRepScore(Node n,
+ Node q,
+ int index,
+ TypeNode v_tn)
+{
if( options::cbqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){ //reject
return -2;
}else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type
}
}
}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
#ifndef __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
#define __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
+#include "context/cdo.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
-// TODO : (as part of #1171, #1214) further document and clean this class.
-/** equality query object using theory engine */
+/** EqualityQueryQuantifiersEngine class
+* This is a wrapper class around an equality engine that is used for
+* queries required by algorithms in the quantifiers theory.
+* It uses an equality engine, as determined by the quantifiers engine it points
+* to.
+*
+* The main extension of this class wrt EqualityQuery is the function
+* getInternalRepresentative, which is used by instantiation-based methods
+* that are agnostic with respect to choosing terms within an equivalence class.
+* Examples of such methods are finite model finding and enumerative
+* instantiation.
+* Method getInternalRepresentative returns the "best" representative based on
+* the internal heuristic,
+* which is currently based on choosing the term that was previously chosen as a
+* representative
+* earliest.
+*/
class EqualityQueryQuantifiersEngine : public EqualityQuery
{
-private:
+ public:
+ EqualityQueryQuantifiersEngine(context::Context* c, QuantifiersEngine* qe);
+ virtual ~EqualityQueryQuantifiersEngine();
+ /** reset */
+ virtual bool reset(Theory::Effort e);
+ /* Called for new quantifiers */
+ virtual void registerQuantifier(Node q) {}
+ /** identify */
+ virtual std::string identify() const { return "EqualityQueryQE"; }
+ /** does the equality engine have term a */
+ bool hasTerm(Node a);
+ /** get the representative of a */
+ Node getRepresentative(Node a);
+ /** are a and b equal? */
+ bool areEqual(Node a, Node b);
+ /** are a and b disequal? */
+ bool areDisequal(Node a, Node b);
+ /** get equality engine
+ * This may either be the master equality engine or the model's equality
+ * engine.
+ */
+ eq::EqualityEngine* getEngine();
+ /** get list of members in the equivalence class of a */
+ void getEquivalenceClass(Node a, std::vector<Node>& eqc);
+ /** get congruent term
+ * If possible, returns a term n such that:
+ * (1) n is a term in the equality engine from getEngine().
+ * (2) n is of the form f( t1, ..., tk ) where ti is in the equivalence class
+ * of args[i] for i=1...k
+ * Otherwise, returns the null node.
+ *
+ * Notice that f should be a "match operator", returned by
+ * TermDb::getMatchOperator.
+ */
+ TNode getCongruentTerm(Node f, std::vector<TNode>& args);
+ /** gets the current best representative in the equivalence
+ * class of a, based on some heuristic. Currently, the default heuristic
+ * chooses terms that were previously chosen as representatives
+ * on the earliest instantiation round.
+ *
+ * If q is non-null, then q/index is the quantified formula
+ * and variable position that we are choosing for instantiation.
+ *
+ * This function avoids certain terms that are "ineligible" for instantiation.
+ * If cbqi is active, we terms that contain instantiation constants
+ * are ineligible. As a result, this function may return
+ * Node::null() if all terms in the equivalence class of a
+ * are ineligible.
+ */
+ Node getInternalRepresentative(Node a, Node q, int index);
+
+ private:
/** pointer to theory engine */
QuantifiersEngine* d_qe;
/** quantifiers equality inference */
std::map< TypeNode, std::map< Node, Node > > d_int_rep;
/** rep score */
std::map< Node, int > d_rep_score;
- /** reset count */
+ /** the number of times reset( e ) has been called */
int d_reset_count;
-
/** processInferences : will merge equivalence classes in master equality engine, if possible */
bool processInferences( Theory::Effort e );
/** node contains */
int getRepScore( Node n, Node f, int index, TypeNode v_tn );
/** flatten representatives */
void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
-public:
- EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe );
- virtual ~EqualityQueryQuantifiersEngine();
- /** reset */
- bool reset( Theory::Effort e );
- /** identify */
- std::string identify() const { return "EqualityQueryQE"; }
- /** general queries about equality */
- bool hasTerm( Node a );
- Node getRepresentative( Node a );
- bool areEqual( Node a, Node b );
- bool areDisequal( Node a, Node b );
- eq::EqualityEngine* getEngine();
- void getEquivalenceClass( Node a, std::vector< Node >& eqc );
- TNode getCongruentTerm( Node f, std::vector< TNode >& args );
- /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
- If cbqi is active, this will return a term in the equivalence class of "a" that does
- not contain instantiation constants, if such a term exists.
- */
- Node getInternalRepresentative( Node a, Node f, int index );
}; /* EqualityQueryQuantifiersEngine */
}/* CVC4::theory::quantifiers namespace */
struct ModelBasisArgSort
{
std::vector< Node > d_terms;
+ // number of arguments that are model-basis terms
+ std::unordered_map<Node, unsigned, NodeHashFunction> d_mba_count;
bool operator() (int i,int j) {
- return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <
- d_terms[j].getAttribute(ModelBasisArgAttribute()) );
+ return (d_mba_count[d_terms[i]] < d_mba_count[d_terms[j]]);
}
};
std::vector< int > indices;
ModelBasisArgSort mbas;
for (int i=0; i<(int)conds.size(); i++) {
- d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );
mbas.d_terms.push_back(conds[i]);
+ mbas.d_mba_count[conds[i]] =
+ d_qe->getTermDatabase()->getModelBasisArg(conds[i]);
indices.push_back(i);
}
std::sort( indices.begin(), indices.end(), mbas );
EqualityQueryInstProp( QuantifiersEngine* qe );
~EqualityQueryInstProp(){};
/** reset */
- bool reset( Theory::Effort e );
+ virtual bool reset(Theory::Effort e);
+ /* Called for new quantifiers */
+ virtual void registerQuantifier(Node q) {}
/** identify */
- std::string identify() const { return "EqualityQueryInstProp"; }
+ virtual std::string identify() const { return "EqualityQueryInstProp"; }
/** extends engine */
bool extendsEngine() { return true; }
/** contains term */
InstPropagator( QuantifiersEngine* qe );
~InstPropagator(){}
/** reset */
- bool reset( Theory::Effort e );
+ virtual bool reset(Theory::Effort e) override;
+ /* Called for new quantifiers */
+ virtual void registerQuantifier(Node q) override {}
/** identify */
- std::string identify() const { return "InstPropagator"; }
+ virtual std::string identify() const override { return "InstPropagator"; }
/** get the notify mechanism */
InstantiationNotify* getInstantiationNotify() { return &d_notify; }
};
#include <iostream>
#include <map>
+#include <vector>
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
class TermUtil;
}
+/** QuantifiersModule class
+*
+* This is the virtual class for defining subsolvers of the quantifiers theory.
+* It has a similar interface to a Theory object.
+*/
class QuantifiersModule {
-protected:
- QuantifiersEngine* d_quantEngine;
public:
QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
virtual ~QuantifiersModule(){}
- //get quantifiers engine
- QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
- /** presolve */
+ /** Presolve.
+ *
+ * Called at the beginning of check-sat call.
+ */
virtual void presolve() {}
- /* whether this module needs to check this round */
+ /** Needs check.
+ *
+ * Returns true if this module wishes a call to be made
+ * to check(e) during QuantifiersEngine::check(e).
+ */
virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
- /* whether this module needs a model built */
+ /** Needs model.
+ *
+ * Whether this module needs a model built during a
+ * call to QuantifiersEngine::check(e)
+ * It returns one of QEFFORT_* from quantifiers_engine.h,
+ * which specifies the quantifiers effort in which it requires the model to
+ * be built.
+ */
virtual unsigned needsModel( Theory::Effort e );
- /* reset at a round */
+ /** Reset.
+ *
+ * Called at the beginning of QuantifiersEngine::check(e).
+ */
virtual void reset_round( Theory::Effort e ){}
- /* Call during quantifier engine's check */
+ /** Check.
+ *
+ * Called during QuantifiersEngine::check(e) depending
+ * if needsCheck(e) returns true.
+ */
virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
- /* check was complete, return false if there is no way to answer "SAT", true if maybe can answer "SAT" */
+ /** Check complete?
+ *
+ * Returns false if the module's reasoning was globally incomplete
+ * (e.g. "sat" must be replaced with "incomplete").
+ *
+ * This is called just before the quantifiers engine will return
+ * with no lemmas added during a LAST_CALL effort check.
+ */
virtual bool checkComplete() { return true; }
- /* check was complete for quantified formula q (e.g. no lemmas implies a model) */
+ /** Check was complete for quantified formula q
+ *
+ * If for each quantified formula q, some module returns true for
+ * checkCompleteFor( q ),
+ * and no lemmas are added by the quantifiers theory, then we may answer
+ * "sat", unless
+ * we are incomplete for other reasons.
+ */
virtual bool checkCompleteFor( Node q ) { return false; }
- /* Called for new quantified formulas */
+ /** Pre register quantifier.
+ *
+ * Called once for new quantified formulas that are
+ * pre-registered by the quantifiers theory.
+ */
virtual void preRegisterQuantifier( Node q ) { }
- /* Called for new quantifiers after owners are finalized */
+ /** Register quantifier
+ *
+ * Called once for new quantified formulas that are
+ * pre-registered by the quantifiers theory, after
+ * internal ownership of quantified formulas is finalized.
+ */
virtual void registerQuantifier( Node q ) = 0;
- virtual void assertNode( Node n ) {}
- virtual void propagate( Theory::Effort level ){}
+ /** Assert node.
+ *
+ * Called when a quantified formula q is asserted to the quantifiers theory
+ */
+ virtual void assertNode(Node q) {}
+ /* Get the next decision request.
+ *
+ * Identical to Theory::getNextDecisionRequest(...)
+ */
virtual Node getNextDecisionRequest( unsigned& priority ) { return TNode::null(); }
/** Identify this module (for debugging, dynamic configuration, etc..) */
virtual std::string identify() const = 0;
-public:
+ //----------------------------general queries
+ /** get currently used the equality engine */
eq::EqualityEngine * getEqualityEngine();
- bool areDisequal( TNode n1, TNode n2 );
+ /** are n1 and n2 equal in the current used equality engine? */
bool areEqual( TNode n1, TNode n2 );
+ /** are n1 and n2 disequal in the current used equality engine? */
+ bool areDisequal(TNode n1, TNode n2);
+ /** get the representative of n in the current used equality engine */
TNode getRepresentative( TNode n );
+ /** get quantifiers engine that owns this module */
+ QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
+ /** get currently used term database */
quantifiers::TermDb * getTermDatabase();
+ /** get currently used term utility object */
quantifiers::TermUtil * getTermUtil();
+ //----------------------------end general queries
+ protected:
+ /** pointer to the quantifiers engine that owns this module */
+ QuantifiersEngine* d_quantEngine;
};/* class QuantifiersModule */
+/** Quantifiers utility
+*
+* This is a lightweight version of a quantifiers module that does not implement
+* methods
+* for checking satisfiability.
+*/
class QuantifiersUtil {
public:
QuantifiersUtil(){}
virtual ~QuantifiersUtil(){}
- /* reset at a round */
+ /* reset
+ * Called at the beginning of an instantiation round
+ * Returns false if the reset failed. When reset fails, the utility should have
+ * added a lemma
+ * via a call to qe->addLemma. TODO: improve this contract #1163
+ */
virtual bool reset( Theory::Effort e ) = 0;
+ /* Called for new quantifiers */
+ virtual void registerQuantifier(Node q) = 0;
/** Identify this module (for debugging, dynamic configuration, etc..) */
virtual std::string identify() const = 0;
};
static void debugPrintMonomialSum(std::map<Node, Node>& msum, const char* c);
};
-
-class QuantRelevance
+/** QuantRelevance
+* This class is used for implementing SinE-style heuristics (e.g. see Hoder et
+* al CADE 2011)
+* This is enabled by the option --relevant-triggers.
+*/
+class QuantRelevance : public QuantifiersUtil
{
private:
/** for computing relevance */
public:
QuantRelevance( bool cr ) : d_computeRel( cr ){}
~QuantRelevance(){}
- /** register quantifier */
- void registerQuantifier( Node f );
+ virtual bool reset(Theory::Effort e) override { return true; }
+ /** Called for new quantifiers after ownership of quantified formulas are
+ * finalized */
+ virtual void registerQuantifier(Node q) override;
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ virtual std::string identify() const override { return "QuantRelevance"; }
/** set relevance */
void setRelevance( Node s, int r );
/** get relevance */
static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
};
-
+/** EqualityQuery
+* This is a wrapper class around equality engine.
+*/
class EqualityQuery : public QuantifiersUtil {
public:
EqualityQuery(){}
virtual eq::EqualityEngine* getEngine() = 0;
/** get the equivalence class of a */
virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
- /** get the term that exists in EE that is congruent to f with args (f is returned by TermDb::getMatchOperator(...) */
+ /** get the term that exists in EE that is congruent to f with args (f is
+ * returned by TermDb::getMatchOperator(...)) */
virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0;
};/* class EqualityQuery */
#include "theory/quantifiers/term_util.h"
using namespace std;
-using namespace CVC4;
using namespace CVC4::kind;
using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) :
d_quantEngine(qe) {
}
Node QuantAttributes::getRewriteRule( Node q ) {
- if( q.getKind()==FORALL && q.getNumChildren()==3 && q[2].getNumChildren()>0 && q[2][0][0].getKind()==REWRITE_RULE ){
+ if (q.getKind() == FORALL && q.getNumChildren() == 3
+ && q[2][0].getNumChildren() > 0
+ && q[2][0][0].getKind() == REWRITE_RULE)
+ {
return q[2][0][0];
}else{
return Node::null();
Node QuantAttributes::getFunDefHead( Node q ) {
//&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF &&
if( q.getKind()==FORALL && q.getNumChildren()==3 ){
-
- for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
- if( q[2][i].getKind()==INST_ATTRIBUTE ){
- if( q[2][i][0].getAttribute(FunDefAttribute()) ){
- return q[2][i][0];
- }
+ Node ipl = q[2];
+ for (unsigned i = 0; i < ipl.getNumChildren(); i++)
+ {
+ if (ipl[i].getKind() == INST_ATTRIBUTE
+ && ipl[i][0].getAttribute(FunDefAttribute()))
+ {
+ return ipl[i][0];
}
}
}
Node f = d_qattr[q].d_fundef_f;
if( d_fun_defs.find( f )!=d_fun_defs.end() ){
Message() << "Cannot define function " << f << " more than once." << std::endl;
- exit( 1 );
+ AlwaysAssert(false);
}
d_fun_defs[f] = true;
d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 );
}
}
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
//struct RrPriorityAttributeId {};
//typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute;
-
-/** This class stores attributes for quantified formulas
-* TODO : document (as part of #1171, #1215)
-*/
-class QAttributes{
-public:
+/** This struct stores attributes for a single quantified formula */
+struct QAttributes
+{
+ public:
QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false),
d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
~QAttributes(){}
+ /** does the quantified formula have a pattern? */
bool d_hasPattern;
+ /** if non-null, this is the rewrite rule representation of the quantified
+ * formula */
Node d_rr;
+ /** is this formula marked a conjecture? */
bool d_conjecture;
+ /** is this formula marked an axiom? */
bool d_axiom;
+ /** if non-null, this quantified formula is a function definition for function
+ * d_fundef_f */
Node d_fundef_f;
+ /** is this formula marked as a sygus conjecture? */
bool d_sygus;
+ /** is this formula marked as a synthesis (non-sygus) conjecture? */
bool d_synthesis;
+ /** if a rewrite rule, then this is the priority value for the rewrite rule */
int d_rr_priority;
+ /** stores the maximum instantiation level allowed for this quantified formula
+ * (-1 means allow any) */
int d_qinstLevel;
+ /** is this formula marked for quantifier elimination? */
bool d_quant_elim;
+ /** is this formula marked for partial quantifier elimination? */
bool d_quant_elim_partial;
+ /** the instantiation pattern list for this quantified formula (its 3rd child)
+ */
Node d_ipl;
+ /** the quantifier id associated with this formula */
Node d_qid_num;
+ /** is this quantified formula a rewrite rule? */
bool isRewriteRule() { return !d_rr.isNull(); }
+ /** is this quantified formula a function definition? */
bool isFunDef() { return !d_fundef_f.isNull(); }
};
-/** This class caches information about attributes of quantified formulas
-* It also has static utility functions used for determining attributes and information about
+/** This class caches information about attributes of quantified formulas
+*
+* It also has static utility functions used for determining attributes and
+* information about
* quantified formulas.
*/
class QuantAttributes
public:
QuantAttributes( QuantifiersEngine * qe );
~QuantAttributes(){}
-
/** set user attribute
- * This function will apply a custom set of attributes to all top-level universal
- * quantifiers contained in n
- */
- static void setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value );
-
- //general queries concerning quantified formulas wrt modules
+ * This function applies an attribute
+ * This can be called when we mark expressions with attributes, e.g. (! q
+ * :attribute attr [node_values, str_value...]),
+ * It can also be called internally in various ways (for SyGus, quantifier
+ * elimination, etc.)
+ */
+ static void setUserAttribute(const std::string& attr,
+ Node q,
+ std::vector<Node>& node_values,
+ std::string str_value);
+
+ /** compute quantifier attributes */
+ static void computeQuantAttributes(Node q, QAttributes& qa);
+ /** compute the attributes for q */
+ void computeAttributes(Node q);
+
/** is quantifier treated as a rewrite rule? */
static bool checkRewriteRule( Node q );
/** get the rewrite rule associated with the quanfied formula */
int getQuantIdNum( Node q );
/** get quant id num */
Node getQuantIdNumNode( Node q );
- /** compute quantifier attributes */
- static void computeQuantAttributes( Node q, QAttributes& qa );
- /** compute the attributes for q */
- void computeAttributes( Node q );
+
private:
/** pointer to quantifiers engine */
QuantifiersEngine * d_quantEngine;
return true;
}
+void RelevantDomain::registerQuantifier(Node q) {}
void RelevantDomain::compute(){
if( !d_is_computed ){
d_is_computed = true;
Trace("rel-dom-debug") << "account for ground terms" << std::endl;
TermDb * db = d_qe->getTermDatabase();
- for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){
- Node op = it->first;
+ for (unsigned k = 0; k < db->getNumOperators(); k++)
+ {
+ Node op = db->getOperator(k);
unsigned sz = db->getNumGroundTerms( op );
for( unsigned i=0; i<sz; i++ ){
- Node n = it->second[i];
+ Node n = db->getGroundTerm(op, i);
//if it is a non-redundant term
if( db->isTermActive( n ) ){
for( unsigned j=0; j<n.getNumChildren(); j++ ){
namespace theory {
namespace quantifiers {
+/** Relevant Domain
+ *
+ * This class computes the relevant domain of
+ * functions and quantified formulas based on
+ * techniques from "Complete Instantiation for Quantified
+ * Formulas in SMT" by Ge et al., CAV 2009.
+ *
+ * Calling compute() will compute a representation
+ * of relevant domain information, which be accessed
+ * by getRDomain(...) calls. It is intended to be called
+ * at full effort check, after we have initialized
+ * the term database.
+ */
class RelevantDomain : public QuantifiersUtil
{
-private:
+ public:
+ RelevantDomain(QuantifiersEngine* qe);
+ virtual ~RelevantDomain();
+ /** Reset. */
+ virtual bool reset(Theory::Effort e) override;
+ /** Register the quantified formula q */
+ virtual void registerQuantifier(Node q) override;
+ /** identify */
+ virtual std::string identify() const override { return "RelevantDomain"; }
+ /** Compute the relevant domain */
+ void compute();
+ /** Relevant domain representation.
+ *
+ * This data structure is inspired by the paper
+ * "Complete Instantiation for Quantified Formulas in SMT" by
+ * Ge et al., CAV 2009.
+ * Notice that relevant domains may be equated to one another,
+ * for example, if the quantified formula forall x. P( x, x )
+ * exists in the current context, then the relevant domain of
+ * arguments 1 and 2 of P are equated.
+ */
class RDomain
{
public:
RDomain() : d_parent( NULL ) {}
- void reset() { d_parent = NULL; d_terms.clear(); }
- RDomain * d_parent;
+ /** the set of terms in this relevant domain */
std::vector< Node > d_terms;
+ /** reset this object */
+ void reset()
+ {
+ d_parent = NULL;
+ d_terms.clear();
+ }
+ /** merge this with r
+ * This sets d_parent of this to r and
+ * copies the terms of this to r.
+ */
void merge( RDomain * r );
+ /** add term to the relevant domain */
void addTerm( Node t );
+ /** get the parent of this */
RDomain * getParent();
+ /** remove redundant terms for d_terms, removes
+ * duplicates modulo equality.
+ */
void removeRedundantTerms( QuantifiersEngine * qe );
+ /** is n in this relevant domain? */
bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); }
+
+ private:
+ /** the parent of this relevant domain */
+ RDomain* d_parent;
};
+ /** get the relevant domain
+ *
+ * Gets object representing the relevant domain of the i^th argument of n.
+ *
+ * If getParent is true, we return the representative
+ * of the equivalence class of relevant domain objects,
+ * which is computed as a union find (see RDomain::d_parent).
+ */
+ RDomain* getRDomain(Node n, int i, bool getParent = true);
+
+ private:
+ /** the relevant domains for each quantified formula and function,
+ * for each variable # and argument #.
+ */
std::map< Node, std::map< int, RDomain * > > d_rel_doms;
+ /** stores the function or quantified formula associated with
+ * each relevant domain object.
+ */
std::map< RDomain *, Node > d_rn_map;
+ /** stores the argument or variable number associated with
+ * each relevant domain object.
+ */
std::map< RDomain *, int > d_ri_map;
+ /** Quantifiers engine associated with this utility. */
QuantifiersEngine* d_qe;
- void computeRelevantDomain( Node q, Node n, bool hasPol, bool pol );
- void computeRelevantDomainOpCh( RDomain * rf, Node n );
+ /** have we computed the relevant domain on this full effort check? */
bool d_is_computed;
-
- //what each literal does
+ /** relevant domain literal
+ * Caches the effect of literals on the relevant domain.
+ */
class RDomainLit {
public:
RDomainLit() : d_merge(false){
d_rd[1] = NULL;
}
~RDomainLit(){}
+ /** whether this literal forces the merge of two relevant domains */
bool d_merge;
+ /** the relevant domains that are merged as a result
+ * of this literal
+ */
RDomain * d_rd[2];
+ /** the terms that are added to
+ * the relevant domain as a result of this literal
+ */
std::vector< Node > d_val;
};
+ /** Cache of the effect of literals on the relevant domain */
std::map< bool, std::map< bool, std::map< Node, RDomainLit > > > d_rel_dom_lit;
+ /** Compute the relevant domain for a subformula n of q,
+ * whose polarity is given by hasPol/pol.
+ */
+ void computeRelevantDomain(Node q, Node n, bool hasPol, bool pol);
+ /** Compute the relevant domain when the term n
+ * is in a position to be included in relevant domain rf.
+ */
+ void computeRelevantDomainOpCh(RDomain* rf, Node n);
+ /** compute relevant domain for literal.
+ *
+ * Updates the relevant domains based on a literal n in quantified
+ * formula q whose polarity is given by hasPol/pol.
+ */
void computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n );
-public:
- RelevantDomain( QuantifiersEngine* qe );
- virtual ~RelevantDomain();
- /* reset */
- bool reset( Theory::Effort e );
- /** identify */
- std::string identify() const { return "RelevantDomain"; }
- //compute the relevant domain
- void compute();
-
- RDomain * getRDomain( Node n, int i, bool getParent = true );
};/* class RelevantDomain */
}
}
+unsigned TermDb::getNumOperators() { return d_ops.size(); }
+Node TermDb::getOperator(unsigned i)
+{
+ Assert(i < d_ops.size());
+ return d_ops[i];
+}
+
/** ground terms */
unsigned TermDb::getNumGroundTerms( Node f ) {
std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f );
Node op = getMatchOperator( n );
Trace("term-db-debug") << " match operator is : " << op << std::endl;
+ d_ops.push_back(op);
d_op_map[op].push_back( n );
added.insert( n );
void TermDb::presolve() {
if( options::incrementalSolving() ){
- //reset the caches that are SAT context-independent
+ // reset the caches that are SAT context-independent but user
+ // context-dependent
+ d_ops.clear();
d_op_map.clear();
d_type_map.clear();
d_processed.clear();
}
}
+unsigned TermDb::getModelBasisArg(Node n)
+{
+ computeModelBasisArgAttribute(n);
+ return n.getAttribute(ModelBasisArgAttribute());
+}
+
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
namespace quantifiers {
+/** Term arg trie class
+*
+* This also referred to as a "term index" or a "signature table".
+*
+* This data structure stores a set expressions, indexed by representatives of
+* their arguments.
+*
+* For example, consider the equivalence classes :
+*
+* { a, d, f( d, c ), f( a, c ) }
+* { b, f( b, d ) }
+* { c, f( b, b ) }
+*
+* where the first elements ( a, b, c ) are the representatives of these classes.
+* The TermArgTrie t we may build for f is :
+*
+* t :
+* t.d_data[a] :
+* t.d_data[a].d_data[c] :
+* t.d_data[a].d_data[c].d_data[f(d,c)] : (leaf)
+* t.d_data[b] :
+* t.d_data[b].d_data[b] :
+* t.d_data[b].d_data[b].d_data[f(b,b)] : (leaf)
+* t.d_data[b].d_data[d] :
+* t.d_data[b].d_data[d].d_data[f(b,d)] : (leaf)
+*
+* Leaf nodes store the terms that are indexed by the arguments, for example
+* term f(d,c) is indexed by the representative arguments (a,c), and is stored
+* as a the (single) key in the data of t.d_data[a].d_data[c].
+*/
class TermArgTrie {
public:
/** the data */
std::map< TNode, TermArgTrie > d_data;
public:
- bool hasNodeData() { return !d_data.empty(); }
- TNode getNodeData() { return d_data.begin()->first; }
- TNode existsTerm( std::vector< TNode >& reps, int argIndex = 0 );
- TNode addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 );
- bool addTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 );
- void debugPrint( const char * c, Node n, unsigned depth = 0 );
- void clear() { d_data.clear(); }
+ /** for leaf nodes : does this trie have data? */
+ bool hasNodeData() { return !d_data.empty(); }
+ /** for leaf nodes : get term corresponding to this leaf */
+ TNode getNodeData() { return d_data.begin()->first; }
+ /** exists term
+ * Returns the term that is indexed by reps, if one exists, or
+ * or returns null otherwise.
+ */
+ TNode existsTerm(std::vector<TNode>& reps, int argIndex = 0);
+ /** add or get term
+ * Returns the term that is previously indexed by reps, if one exists, or
+ * Adds n to the trie, indexed by reps, and returns n.
+ */
+ TNode addOrGetTerm(TNode n, std::vector<TNode>& reps, int argIndex = 0);
+ /** add term
+ * Returns false if a term is previously indexed by reps.
+ * Returns true if no term is previously indexed by reps,
+ * and adds n to the trie, indexed by reps, and returns n.
+ */
+ bool addTerm(TNode n, std::vector<TNode>& reps, int argIndex = 0);
+ /** debug print this trie */
+ void debugPrint(const char* c, Node n, unsigned depth = 0);
+ /** clear all data from this trie */
+ void clear() { d_data.clear(); }
};/* class TermArgTrie */
namespace fmcheck {
class TermGenerator;
class TermGenEnv;
+/** Term Database
+*
+* The primary responsibilities for this class are to :
+* (1) Maintain a list of all ground terms that exist in the quantifier-free
+* solvers, as notified through the master equality engine.
+* (2) Build TermArgTrie objects that index all ground terms, per operator. This
+* is done lazily, for performance reasons.
+*/
class TermDb : public QuantifiersUtil {
friend class ::CVC4::theory::QuantifiersEngine;
- //TODO: eliminate most of these
- friend class ::CVC4::theory::inst::Trigger;
- friend class ::CVC4::theory::inst::HigherOrderTrigger;
- friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker;
- friend class ::CVC4::theory::quantifiers::QuantConflictFind;
- friend class ::CVC4::theory::quantifiers::RelevantDomain;
+ // TODO: eliminate these
friend class ::CVC4::theory::quantifiers::ConjectureGenerator;
friend class ::CVC4::theory::quantifiers::TermGenEnv;
typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
-private:
+
+ public:
+ TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe);
+ ~TermDb();
+ /** presolve (called once per user check-sat) */
+ void presolve();
+ /** reset (calculate which terms are active) */
+ virtual bool reset(Theory::Effort effort) override;
+ /** register quantified formula */
+ virtual void registerQuantifier(Node q) override;
+ /** identify */
+ virtual std::string identify() const override { return "TermDb"; }
+ /** get number of operators */
+ unsigned getNumOperators();
+ /** get operator at index i */
+ Node getOperator(unsigned i);
+ /** ground terms for operator
+ * Get the number of ground terms with operator f that have been added to the
+ * database
+ */
+ unsigned getNumGroundTerms(Node f);
+ /** get ground term for operator
+ * Get the i^th ground term with operator f that has been added to the database
+ */
+ Node getGroundTerm(Node f, unsigned i);
+ /** get num type terms
+ * Get the number of ground terms of tn that have been added to the database
+ */
+ unsigned getNumTypeGroundTerms(TypeNode tn);
+ /** get type ground term
+ * Returns the i^th ground term of type tn
+ */
+ Node getTypeGroundTerm(TypeNode tn, unsigned i);
+ /** 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);
+ /** get match operator for term n
+ *
+ * If n has a kind that we index, this function will
+ * typically return n.getOperator().
+ *
+ * However, for parametric operators f, the match operator is an arbitrary
+ * chosen f-application. For example, consider array select:
+ * A : (Array Int Int)
+ * B : (Array Bool Int)
+ * We require that terms like (select A 1) and (select B 2) are indexed in
+ * separate
+ * data structures despite the fact that
+ * (select A 1).getOperator()==(select B 2).getOperator().
+ * Hence, for the above terms, we may return:
+ * getMatchOperator( (select A 1) ) = (select A 1), and
+ * getMatchOperator( (select B 2) ) = (select B 2).
+ * The match operator is the first instance of an application of the parametric
+ * operator of its type.
+ *
+ * If n has a kind that we do not index (like PLUS),
+ * then this function returns Node::null().
+ */
+ Node getMatchOperator(Node n);
+ /** get term arg index for all f-applications in the current context */
+ TermArgTrie* getTermArgTrie(Node f);
+ /** get the term arg trie for f-applications in the equivalence class of eqc.
+ */
+ TermArgTrie* getTermArgTrie(Node eqc, Node f);
+ /** get congruent term
+ * If possible, returns a term t such that:
+ * (1) t is a term that is currently indexed by this database,
+ * (2) t is of the form f( t1, ..., tk )
+ */
+ TNode getCongruentTerm(Node f, Node n);
+ /** get congruent term
+ * If possible, returns a term t such that:
+ * (1) t is a term that is currently indexed by this database,
+ * (2) t is of the form f( t1, ..., tk ) and n is of the form f( s1, ..., sk ),
+ * where ti is in the equivalence class of si for i=1...k
+ */
+ TNode getCongruentTerm(Node f, std::vector<TNode>& args);
+ /** in relevant domain
+ * Returns true if there is at least one term t such that:
+ * (1) t is a term that is currently indexed by this database,
+ * (2) t is of the form f( t1, ..., tk ) and ti is in the equivalence class of
+ * r.
+ */
+ bool inRelevantDomain(TNode f, unsigned i, TNode r);
+ /** evaluate term
+ *
+ * Returns a term n' such that n = n' is entailed based on the equality
+ * information qy. This function may generate new terms. In particular,
+ * we typically rewrite maximal
+ * subterms of n to terms that exist in the equality engine specified by qy.
+ *
+ * useEntailmentTests is whether to use the theory engine's entailmentCheck
+ * call, for increased precision. This is not frequently used.
+ */
+ Node evaluateTerm(TNode n,
+ EqualityQuery* qy = NULL,
+ bool useEntailmentTests = false);
+ /** get entailed term
+ *
+ * If possible, returns a term n' such that:
+ * (1) n' exists in the current equality engine (as specified by qy),
+ * (2) n = n' is entailed in the current context.
+ * It returns null if no such term can be found.
+ * Wrt evaluateTerm, this version does not construct new terms, and
+ * thus is less aggressive.
+ */
+ TNode getEntailedTerm(TNode n, EqualityQuery* qy = NULL);
+ /** get entailed term
+ *
+ * If possible, returns a term n' such that:
+ * (1) n' exists in the current equality engine (as specified by qy),
+ * (2) n * subs = n' is entailed in the current context, where * is denotes
+ * substitution application.
+ * It returns null if no such term can be found.
+ * subsRep is whether the substitution maps to terms that are representatives
+ * according to qy.
+ * Wrt evaluateTerm, this version does not construct new terms, and
+ * thus is less aggressive.
+ */
+ TNode getEntailedTerm(TNode n,
+ std::map<TNode, TNode>& subs,
+ bool subsRep,
+ EqualityQuery* qy = NULL);
+ /** is entailed
+ * Checks whether the current context entails n with polarity pol, based on the
+ * equality information qy.
+ * Returns true if the entailment can be successfully shown.
+ */
+ bool isEntailed(TNode n, bool pol, EqualityQuery* qy = NULL);
+ /** is entailed
+ *
+ * Checks whether the current context entails ( n * subs ) with polarity pol,
+ * based on the equality information qy,
+ * where * denotes substitution application.
+ * subsRep is whether the substitution maps to terms that are representatives
+ * according to qy.
+ */
+ bool isEntailed(TNode n,
+ std::map<TNode, TNode>& subs,
+ bool subsRep,
+ bool pol,
+ EqualityQuery* qy = NULL);
+ /** is the term n active in the current context?
+ *
+ * By default, all terms are active. A term is inactive if:
+ * (1) it is congruent to another term
+ * (2) it is irrelevant based on the term database mode. This includes terms
+ * that only appear in literals that are not relevant.
+ * (3) it contains instantiation constants (used for CEGQI and cannot be used
+ * in instantiation).
+ * (4) it is explicitly set inactive by a call to setTermInactive(...).
+ * We store whether a term is inactive in a SAT-context-dependent map.
+ */
+ bool isTermActive(Node n);
+ /** set that term n is inactive in this context. */
+ void setTermInactive(Node n);
+ /** has term current
+ *
+ * This function is used in cases where we restrict which terms appear in the
+ * database, such as for heuristics used in local theory extensions
+ * and for --term-db-mode=relevant.
+ * It returns whether the term n should be indexed in the current context.
+ */
+ bool hasTermCurrent(Node n, bool useMode = true);
+ /** is term eligble for instantiation? */
+ bool isTermEligibleForInstantiation(TNode n, TNode f, bool print = false);
+ /** get eligible term in equivalence class */
+ Node getEligibleTermInEqc(TNode r);
+ /** is inst closure */
+ bool isInstClosure(Node r);
+
+ private:
/** reference to the quantifiers engine */
QuantifiersEngine* d_quantEngine;
/** terms processed */
/** boolean terms */
Node d_true;
Node d_false;
-public:
- TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe);
- ~TermDb();
-
- /** register quantified formula */
- void registerQuantifier( Node q );
-public:
- /** presolve (called once per user check-sat) */
- void presolve();
- /** reset (calculate which terms are active) */
- bool reset( Theory::Effort effort );
- /** identify */
- std::string identify() const { return "TermDb"; }
-private:
+ /** list of all operators */
+ std::vector<Node> d_ops;
/** map from operators to ground terms for that operator */
std::map< Node, std::vector< Node > > d_op_map;
/** map from type nodes to terms of that type */
std::map< TypeNode, std::vector< Node > > d_type_map;
/** inactive map */
NodeBoolMap d_inactive_map;
-
- /** count number of non-redundant ground terms per operator */
+ /** count of the number of non-redundant ground terms per operator */
std::map< Node, int > d_op_nonred_count;
- /**mapping from UF terms to representatives of their arguments */
+ /** mapping from terms to representatives of their arguments */
std::map< TNode, std::vector< TNode > > d_arg_reps;
/** map from operators to trie */
std::map< Node, TermArgTrie > d_func_map_trie;
std::map< Node, Node > d_term_elig_eqc;
/** set has term */
void setHasTerm( Node n );
- /** evaluate term */
+ /** helper for evaluate term */
Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests );
+ /** helper for get entailed term */
TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
+ /** helper for is entailed */
bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
- /** compute uf eqc terms */
+ /** compute uf eqc terms :
+ * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes
+ */
void computeUfEqcTerms( TNode f );
- /** compute uf terms */
+ /** compute uf terms
+ * Ensure that an entry for f is in d_func_map_trie
+ */
void computeUfTerms( TNode f );
-private: // for higher-order term indexing
+ /** compute arg reps
+ * Ensure that an entry for n is in d_arg_reps
+ */
+ void computeArgReps(TNode n);
+ //------------------------------higher-order term indexing
/** a map from matchable operators to their representative */
std::map< TNode, TNode > d_ho_op_rep;
/** for each representative matchable operator, the list of other matchable operators in their equivalence class */
std::map< TNode, std::vector< TNode > > d_ho_op_rep_slaves;
/** get operator representative */
Node getOperatorRepresentative( TNode op ) const;
-public:
- /** ground terms for operator */
- unsigned getNumGroundTerms( Node f );
- /** get ground term for operator */
- Node getGroundTerm( Node f, unsigned i );
- /** get num type terms */
- unsigned getNumTypeGroundTerms( TypeNode tn );
- /** get type ground term */
- Node getTypeGroundTerm( TypeNode tn, unsigned i );
- /** add a term to the database */
- void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false );
- /** get match operator */
- Node getMatchOperator( Node n );
- /** get term arg index */
- TermArgTrie * getTermArgTrie( Node f );
- TermArgTrie * getTermArgTrie( Node eqc, Node f );
- /** exists term */
- TNode getCongruentTerm( Node f, Node n );
- TNode getCongruentTerm( Node f, std::vector< TNode >& args );
- /** compute arg reps */
- void computeArgReps( TNode n );
- /** in relevant domain */
- bool inRelevantDomain( TNode f, unsigned i, TNode r );
- /** evaluate a term under a substitution. Return representative in EE if possible.
- * subsRep is whether subs contains only representatives
- */
- Node evaluateTerm( TNode n, EqualityQuery * qy = NULL, bool useEntailmentTests = false );
- /** get entailed term, does not construct new terms, less aggressive */
- TNode getEntailedTerm( TNode n, EqualityQuery * qy = NULL );
- TNode getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy = NULL );
- /** is entailed (incomplete check) */
- bool isEntailed( TNode n, bool pol, EqualityQuery * qy = NULL );
- bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL );
- /** is active */
- bool isTermActive( Node n );
- void setTermInactive( Node n );
- /** has term */
- bool hasTermCurrent( Node n, bool useMode = true );
- /** is term eligble for instantiation? */
- bool isTermEligibleForInstantiation( TNode n, TNode f, bool print = false );
- /** get has term eqc */
- Node getEligibleTermInEqc( TNode r );
- /** is inst closure */
- bool isInstClosure( Node r );
-
-//for model basis
-private:
- //map from types to model basis terms
+ //------------------------------end higher-order term indexing
+
+ // TODO : as part of #1171, these should be moved somewhere else
+ // for model basis
+ private:
+ /** map from types to model basis terms */
std::map< TypeNode, Node > d_model_basis_term;
- //map from ops to model basis terms
+ /** map from ops to model basis terms */
std::map< Node, Node > d_model_basis_op_term;
- //map from instantiation terms to their model basis equivalent
+ /** map from instantiation terms to their model basis equivalent */
std::map< Node, Node > d_model_basis_body;
/** map from universal quantifiers to model basis terms */
std::map< Node, std::vector< Node > > d_model_basis_terms;
- // compute model basis arg
+ /** compute model basis arg */
void computeModelBasisArgAttribute( Node n );
-public:
- //get model basis term
- Node getModelBasisTerm( TypeNode tn, int i = 0 );
- //get model basis term for op
- Node getModelBasisOpTerm( Node op );
- //get model basis
- Node getModelBasis( Node q, Node n );
- //get model basis body
- Node getModelBasisBody( Node q );
-
+ public:
+ /** get model basis term */
+ Node getModelBasisTerm(TypeNode tn, int i = 0);
+ /** get model basis term for op */
+ Node getModelBasisOpTerm(Node op);
+ /** get model basis */
+ Node getModelBasis(Node q, Node n);
+ /** get model basis body */
+ Node getModelBasisBody(Node q);
+ /** get model basis arg */
+ unsigned getModelBasisArg(Node n);
+
};/* class TermDb */
}/* CVC4::theory::quantifiers namespace */
#include <unordered_set>
#include "expr/attribute.h"
+#include "theory/quantifiers/quant_util.h"
#include "theory/type_enumerator.h"
namespace CVC4 {
class TermDatabase;
// TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used.
-class TermUtil {
+class TermUtil : public QuantifiersUtil
+{
// TODO : remove these
friend class ::CVC4::theory::QuantifiersEngine;
friend class TermDatabase;
Node d_zero;
Node d_one;
+ /** reset */
+ virtual bool reset(Theory::Effort e) override { return true; }
/** register quantifier */
- void registerQuantifier( Node q );
-
-//for inst constant
-private:
+ virtual void registerQuantifier(Node q) override;
+ /** identify */
+ virtual std::string identify() const override { return "TermUtil"; }
+ // for inst constant
+ private:
/** map from universal quantifiers to the list of variables */
std::map< Node, std::vector< Node > > d_vars;
std::map< Node, std::map< Node, unsigned > > d_var_num;
using namespace CVC4::theory::inst;
QuantifiersEngine::QuantifiersEngine(context::Context* c,
- context::UserContext* u, TheoryEngine* te)
+ context::UserContext* u,
+ TheoryEngine* te)
: d_te(te),
+ d_quant_attr(new quantifiers::QuantAttributes(this)),
d_conflict_c(c, false),
// d_quants(u),
d_quants_red(u),
d_lemmas_produced_c(u),
d_skolemized(u),
- d_quant_attr(new quantifiers::QuantAttributes(this)),
d_ierCounter_c(c),
// d_ierCounter(c),
// d_ierCounter_lc(c),
d_presolve_in(u),
d_presolve_cache(u),
d_presolve_cache_wq(u),
- d_presolve_cache_wic(u) {
+ d_presolve_cache_wic(u)
+{
//utilities
d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this );
d_util.push_back( d_eq_query );
+ // term util must come first
+ d_term_util = new quantifiers::TermUtil(this);
+ d_util.push_back(d_term_util);
+
d_term_db = new quantifiers::TermDb( c, u, this );
d_util.push_back( d_term_db );
- d_term_util = new quantifiers::TermUtil( this );
-
if (options::ceGuidedInst()) {
d_sygus_tdb = new quantifiers::TermDbSygus(c, this);
}else{
if( options::relevantTriggers() ){
d_quant_rel = new QuantRelevance( false );
+ d_util.push_back(d_quant_rel);
}else{
d_quant_rel = NULL;
}
d_quants[f] = false;
return false;
}else{
- // register with utilities : TODO (#1163) make this a standard call
-
- d_term_util->registerQuantifier( f );
- d_term_db->registerQuantifier( f );
- d_quant_attr->computeAttributes( f );
- //register with quantifier relevance
- if( d_quant_rel ){
- d_quant_rel->registerQuantifier( f );
+ // register with utilities
+ for (unsigned i = 0; i < d_util.size(); i++)
+ {
+ d_util[i]->registerQuantifier(f);
}
-
+ // compute attributes
+ d_quant_attr->computeAttributes(f);
+
for( unsigned i=0; i<d_modules.size(); i++ ){
Trace("quant-debug") << "pre-register with " << d_modules[i]->identify() << "..." << std::endl;
d_modules[i]->preRegisterQuantifier( f );
}
//TODO: remove this
Node ceBody = d_term_util->getInstConstantBody( f );
- //also register it with the strong solver
- //if( options::finiteModelFind() ){
- // ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
- //}
Trace("quant-debug") << "...finish." << std::endl;
d_quants[f] = true;
// flush lemmas
void QuantifiersEngine::propagate( Theory::Effort level ){
CodeTimer codeTimer(d_statistics.d_time);
- for( int i=0; i<(int)d_modules.size(); i++ ){
- d_modules[i]->propagate( level );
- }
}
Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){
quantifiers::QModelBuilder* d_builder;
/** utility for effectively propositional logic */
QuantEPR * d_qepr;
-private:
+ /** term database */
+ quantifiers::TermDb* d_term_db;
+ /** sygus term database */
+ quantifiers::TermDbSygus* d_sygus_tdb;
+ /** term utilities */
+ quantifiers::TermUtil* d_term_util;
+ /** quantifiers attributes */
+ std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
+
+ private:
/** instantiation engine */
quantifiers::InstantiationEngine* d_inst_engine;
/** model engine */
quantifiers::QuantAntiSkolem * d_anti_skolem;
/** quantifiers instantiation propagtor */
quantifiers::InstPropagator * d_inst_prop;
-public: //effort levels
+
+ public: // effort levels (TODO : make an enum and use everywhere #1293)
enum {
QEFFORT_CONFLICT,
QEFFORT_STANDARD,
std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst;
/** quantifiers that have been skolemized */
BoolMap d_skolemized;
- /** term database */
- quantifiers::TermDb* d_term_db;
- /** term database */
- quantifiers::TermDbSygus* d_sygus_tdb;
- /** term utilities */
- quantifiers::TermUtil* d_term_util;
- /** quantifiers attributes */
- std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
/** all triggers will be stored in this trie */
inst::TriggerTrie* d_tr_trie;
/** extended model object */
/** if theories want to do something with model after building, do it here */
virtual void postProcessModel( TheoryModel* m ){ }
-
/**
* Return a decision request, if the theory has one, or the NULL node
* otherwise.
- * If returning non-null node, hould set priority to
+ * If returning non-null node, should set priority to
* 0 if decision is necessary for model-soundness,
* 1 if decision is necessary for completeness,
* >1 otherwise.
projects / cvc5.git / commitdiff