* Fix some documentation.
* Move model basis out of term db.
* Moving
* Finished moving.
* Document Skolemize and term enumeration.
* Minor
* Model basis to first order model.
* Change function name.
* Minor
* Clang format.
* Minor
* Format
* Minor
* Format
* Address review.
theory/quantifiers/relevant_domain.h \
theory/quantifiers/rewrite_engine.cpp \
theory/quantifiers/rewrite_engine.h \
+ theory/quantifiers/skolemize.cpp \
+ theory/quantifiers/skolemize.h \
theory/quantifiers/sygus_grammar_cons.cpp \
theory/quantifiers/sygus_grammar_cons.h \
theory/quantifiers/sygus_process_conj.cpp \
theory/quantifiers/term_database.h \
theory/quantifiers/term_database_sygus.cpp \
theory/quantifiers/term_database_sygus.h \
+ theory/quantifiers/term_enumeration.cpp \
+ theory/quantifiers/term_enumeration.h \
theory/quantifiers/term_util.cpp \
theory/quantifiers/term_util.h \
theory/quantifiers/theory_quantifiers.cpp \
** \brief Implementation of abstract MBQI builder
**/
-
-#include "options/quantifiers_options.h"
#include "theory/quantifiers/ambqi_builder.h"
+#include "options/quantifiers_options.h"
#include "theory/quantifiers/term_database.h"
+#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 {
+
void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth ) {
d_def.clear();
}
if( fapps.empty() ){
//choose arbitrary value
- Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);
+ Node mbt = fm->getModelBasisOpTerm(f);
Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl;
fapps.push_back( mbt );
}
return true;
}
}
+
+}/* namespace CVC4::theory::quantifiers */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
** This class manages integer bounds for quantifiers
**/
-#include "options/quantifiers_options.h"
#include "theory/quantifiers/bounded_integers.h"
+#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/model_engine.h"
#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
#include "theory/theory_engine.h"
for( unsigned i=0; i<f[0].getNumChildren(); i++) {
if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
TypeNode tn = f[0][i].getType();
- if( tn.isSort() || getTermUtil()->mayComplete( tn ) ){
+ if (tn.isSort()
+ || d_quantEngine->getTermEnumeration()->mayComplete(tn))
+ {
success = true;
setBoundedVar( f, f[0][i], BOUND_FINITE );
break;
if( d_firstTime ){
//must return something
d_firstTime = false;
- return d_qe->getTermDatabase()->getModelBasisTerm( d_match_pattern_type );
+ return d_qe->getTermForType(d_match_pattern_type);
}
return Node::null();
}
#include "smt/smt_statistics_registry.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/skolemize.h"
#include "theory/quantifiers/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
#include "theory/theory_engine.h"
Node dr = Rewriter::rewrite( d[i] );
if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
if( constructed_cand ){
- ic.push_back( d_qe->getTermUtil()->getSkolemizedBody( dr[0] ).negate() );
+ ic.push_back(d_qe->getSkolemize()->getSkolemizedBody(dr[0]).negate());
}
if( sk_refine ){
Assert( !isGround() );
Node ce_q = d_ce_sk[0][k];
if( !ce_q.isNull() ){
Assert( !d_inner_vars_disj[k].empty() );
- Assert( d_inner_vars_disj[k].size()==d_qe->getTermUtil()->d_skolem_constants[ce_q].size() );
+ std::vector<Node> skolems;
+ d_qe->getSkolemize()->getSkolemConstants(ce_q, skolems);
+ Assert(d_inner_vars_disj[k].size() == skolems.size());
std::vector< Node > model_values;
- getModelValues( d_qe->getTermUtil()->d_skolem_constants[ce_q], model_values );
+ getModelValues(skolems, model_values);
sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() );
sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() );
}else{
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
Node s;
if( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ){
Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl;
- s = d_qe->getTermUtil()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 );
+ s = d_qe->getTermEnumeration()->getEnumerateTerm(
+ TypeNode::fromType(dt.getSygusType()), 0);
}else{
Trace("csi-sol") << "Get solution for " << prog << ", with skolems : ";
sol_index = d_prog_to_sol_index[prog];
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
std::vector< TypeNode > to_erase;
for( std::map< TypeNode, bool >::iterator it = active.begin(); it != active.end(); ++it ){
TypeNode stn = it->first;
- Node ns = d_qe->getTermUtil()->getEnumerateTerm( stn, index );
+ Node ns = d_qe->getTermEnumeration()->getEnumerateTerm(stn, index);
if( ns.isNull() ){
to_erase.push_back( stn );
}else{
#include "options/quantifiers_options.h"
#include "smt/term_formula_removal.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
-
using namespace std;
using namespace CVC4;
using namespace CVC4::kind;
Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){
- d_closed_enum_type = qe->getTermUtil()->isClosedEnumerableType( tn );
+ d_closed_enum_type = qe->getTermEnumeration()->isClosedEnumerableType(tn);
}
**
**/
-#include "options/quantifiers_options.h"
#include "theory/quantifiers/conjecture_generator.h"
+#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/skolemize.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/theory_engine.h"
std::vector< TNode > args;
Trace("sg-pat-debug") << "******* Get ground term for " << r << std::endl;
Node n;
- if( getTermUtil()->isInductionTerm( r ) ){
+ if (Skolemize::isInductionTerm(r))
+ {
n = d_op_arg_index[r].getGroundTerm( this, args );
}else{
n = r;
if( std::find( provenConj.begin(), provenConj.end(), q )==provenConj.end() ){
//check each skolem variable
bool disproven = true;
- //std::vector< Node > sk;
- //getTermUtil()->getSkolemConstants( q, sk, true );
+ std::vector<Node> skolems;
+ d_quantEngine->getSkolemize()->getSkolemConstants(q, skolems);
Trace("sg-conjecture") << " CONJECTURE : ";
std::vector< Node > ce;
- for( unsigned j=0; j<getTermUtil()->d_skolem_constants[q].size(); j++ ){
- TNode k = getTermUtil()->d_skolem_constants[q][j];
+ for (unsigned j = 0; j < skolems.size(); j++)
+ {
+ TNode k = skolems[j];
TNode rk = getRepresentative( k );
std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( rk );
//check if it is a ground term
Trace("sg-conjecture") << "ACTIVE : " << q;
if( Trace.isOn("sg-gen-eqc") ){
Trace("sg-conjecture") << " { ";
- for( unsigned k=0; k<getTermUtil()->d_skolem_constants[q].size(); k++ ){ Trace("sg-conjecture") << getTermUtil()->d_skolem_constants[q][k] << ( j==k ? "*" : "" ) << " "; }
+ for (unsigned k = 0; k < skolems.size(); k++)
+ {
+ Trace("sg-conjecture") << skolems[k] << (j == k ? "*" : "")
+ << " ";
+ }
Trace("sg-conjecture") << "}";
}
Trace("sg-conjecture") << std::endl;
void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {
if( n.getNumChildren()>0 ){
+ TermEnumeration* te = d_quantEngine->getTermEnumeration();
std::vector< int > vec;
std::vector< TypeNode > types;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
vec.push_back( 0 );
TypeNode tn = n[i].getType();
- if( getTermUtil()->isClosedEnumerableType( tn ) ){
+ if (te->isClosedEnumerableType(tn))
+ {
types.push_back( tn );
}else{
return;
vec.push_back( size_limit );
}else{
//see if we can iterate current
- if( vec_sum<size_limit && !getTermUtil()->getEnumerateTerm( types[index], vec[index]+1 ).isNull() ){
+ if (vec_sum < size_limit
+ && !te->getEnumerateTerm(types[index], vec[index] + 1).isNull())
+ {
vec[index]++;
vec_sum++;
vec.push_back( size_limit - vec_sum );
}
if( success ){
if( vec.size()==n.getNumChildren() ){
- Node lc = getTermUtil()->getEnumerateTerm( types[vec.size()-1], vec[vec.size()-1] );
+ Node lc =
+ te->getEnumerateTerm(types[vec.size() - 1], vec[vec.size() - 1]);
if( !lc.isNull() ){
for( unsigned i=0; i<vec.size(); i++ ){
Trace("sg-gt-enum-debug") << vec[i] << " ";
std::vector< Node > children;
children.push_back( n.getOperator() );
for( unsigned i=0; i<(vec.size()-1); i++ ){
- Node nn = getTermUtil()->getEnumerateTerm( types[i], vec[i] );
+ Node nn = te->getEnumerateTerm(types[i], vec[i]);
Assert( !nn.isNull() );
Assert( nn.getType()==n[i].getType() );
children.push_back( nn );
** \brief Implementation of model engine model class
**/
+#include "theory/quantifiers/first_order_model.h"
+#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/ambqi_builder.h"
-#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/full_model_check.h"
#include "theory/quantifiers/model_engine.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
#define USE_INDEX_ORDERING
//check if there is even any domain elements at all
if (!d_rep_set.hasType(tn)) {
Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
- Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+ Node mbt = getModelBasisTerm(tn);
Trace("fmc-model-debug") << "Add to representative set..." << std::endl;
d_rep_set.add(tn, mbt);
}else if( d_rep_set.d_type_reps[tn].size()==0 ){
return std::find( d_forall_rlv_assert.begin(), d_forall_rlv_assert.end(), q )!=d_forall_rlv_assert.end();
}
+Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
+{
+ if (d_model_basis_term.find(tn) == d_model_basis_term.end())
+ {
+ Node mbt;
+ if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn))
+ {
+ mbt = d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
+ }
+ else
+ {
+ if (options::fmfFreshDistConst())
+ {
+ mbt = d_qe->getTermDatabase()->getOrMakeTypeFreshVariable(tn);
+ }
+ else
+ {
+ mbt = d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn);
+ }
+ }
+ ModelBasisAttribute mba;
+ mbt.setAttribute(mba, true);
+ d_model_basis_term[tn] = mbt;
+ Trace("model-basis-term") << "Choose " << mbt << " as model basis term for "
+ << tn << std::endl;
+ }
+ return d_model_basis_term[tn];
+}
+
+bool FirstOrderModel::isModelBasisTerm(Node n)
+{
+ return n == getModelBasisTerm(n.getType());
+}
+
+Node FirstOrderModel::getModelBasisOpTerm(Node op)
+{
+ if (d_model_basis_op_term.find(op) == d_model_basis_op_term.end())
+ {
+ TypeNode t = op.getType();
+ std::vector<Node> children;
+ children.push_back(op);
+ for (int i = 0; i < (int)(t.getNumChildren() - 1); i++)
+ {
+ children.push_back(getModelBasisTerm(t[i]));
+ }
+ if (children.size() == 1)
+ {
+ d_model_basis_op_term[op] = op;
+ }
+ else
+ {
+ d_model_basis_op_term[op] =
+ NodeManager::currentNM()->mkNode(APPLY_UF, children);
+ }
+ }
+ return d_model_basis_op_term[op];
+}
+
+Node FirstOrderModel::getModelBasis(Node q, Node n)
+{
+ // make model basis
+ if (d_model_basis_terms.find(q) == d_model_basis_terms.end())
+ {
+ for (unsigned j = 0; j < q[0].getNumChildren(); j++)
+ {
+ d_model_basis_terms[q].push_back(getModelBasisTerm(q[0][j].getType()));
+ }
+ }
+ Node gn = d_qe->getTermUtil()->substituteInstConstants(
+ n, q, d_model_basis_terms[q]);
+ return gn;
+}
+
+Node FirstOrderModel::getModelBasisBody(Node q)
+{
+ if (d_model_basis_body.find(q) == d_model_basis_body.end())
+ {
+ Node n = d_qe->getTermUtil()->getInstConstantBody(q);
+ d_model_basis_body[q] = getModelBasis(q, n);
+ }
+ return d_model_basis_body[q];
+}
+
+void FirstOrderModel::computeModelBasisArgAttribute(Node n)
+{
+ if (!n.hasAttribute(ModelBasisArgAttribute()))
+ {
+ // ensure that the model basis terms have been defined
+ if (n.getKind() == APPLY_UF)
+ {
+ getModelBasisOpTerm(n.getOperator());
+ }
+ uint64_t val = 0;
+ // determine if it has model basis attribute
+ for (unsigned j = 0; j < n.getNumChildren(); j++)
+ {
+ if (n[j].getAttribute(ModelBasisAttribute()))
+ {
+ val++;
+ }
+ }
+ ModelBasisArgAttribute mbaa;
+ n.setAttribute(mbaa, val);
+ }
+}
+
+unsigned FirstOrderModel::getModelBasisArg(Node n)
+{
+ computeModelBasisArgAttribute(n);
+ return n.getAttribute(ModelBasisArgAttribute());
+}
+
FirstOrderModelIG::FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name) :
FirstOrderModel(qe, c,name) {
return st;
}
-bool FirstOrderModelFmc::isModelBasisTerm(Node n) {
- return n==getModelBasisTerm(n.getType());
-}
-
-Node FirstOrderModelFmc::getModelBasisTerm(TypeNode tn) {
- return d_qe->getTermDatabase()->getModelBasisTerm(tn);
-}
-
Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
Trace("fmc-model") << "Get function value for " << op << std::endl;
TypeNode type = op.getType();
class QuantifiersEngine;
+struct ModelBasisAttributeId
+{
+};
+typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
+// for APPLY_UF terms, 1 : term has direct child with model basis attribute,
+// 0 : term has no direct child with model basis attribute.
+struct ModelBasisArgAttributeId
+{
+};
+typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t>
+ ModelBasisArgAttribute;
+
namespace quantifiers {
class TermDb;
struct IsStarAttributeId {};
typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
+// TODO (#1301) : document and refactor this class
class FirstOrderModel : public TheoryModel
{
-protected:
- /** quant engine */
- QuantifiersEngine * d_qe;
- /** list of quantifiers asserted in the current context */
- context::CDList<Node> d_forall_asserts;
- /** quantified formulas marked as relevant */
- unsigned d_rlv_count;
- std::map< Node, unsigned > d_forall_rlv;
- std::vector< Node > d_forall_rlv_vec;
- Node d_last_forall_rlv;
- std::vector< Node > d_forall_rlv_assert;
- /** get variable id */
- std::map< Node, std::map< Node, int > > d_quant_var_id;
- /** get current model value (deprecated) */
- //virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
-public: //for Theory Quantifiers:
+ public:
+ FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name);
+ virtual ~FirstOrderModel() throw() {}
+ virtual FirstOrderModelIG* asFirstOrderModelIG() { return nullptr; }
+ virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
+ virtual FirstOrderModelQInt* asFirstOrderModelQInt() { return nullptr; }
+ virtual FirstOrderModelAbs* asFirstOrderModelAbs() { return nullptr; }
/** assert quantifier */
void assertQuantifier( Node n );
/** get number of asserted quantifiers */
Node getAssertedQuantifier( unsigned i, bool ordered = false );
/** initialize model for term */
void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
- virtual void processInitializeModelForTerm( Node n ) = 0;
- virtual void processInitializeQuantifier( Node q ) {}
-public:
- FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name );
- virtual ~FirstOrderModel() throw() {}
- virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
- virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
- virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
- virtual FirstOrderModelAbs * asFirstOrderModelAbs() { return NULL; }
// initialize the model
void initialize();
- virtual void processInitialize( bool ispre ) = 0;
/** get variable id */
int getVariableId(TNode q, TNode n) {
return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
}
- /** get some domain element */
- Node getSomeDomainElement(TypeNode tn);
/** do we need to do any work? */
bool checkNeeded();
-private:
- //list of inactive quantified formulas
- std::map< TNode, bool > d_quant_active;
-public:
/** reset round */
void reset_round();
/** mark quantified formula relevant */
bool isQuantifierActive( TNode q );
/** is quantified formula asserted */
bool isQuantifierAsserted( TNode q );
+ /** get model basis term */
+ Node getModelBasisTerm(TypeNode tn);
+ /** is model basis term */
+ bool isModelBasisTerm(Node n);
+ /** 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);
+ /** get some domain element */
+ Node getSomeDomainElement(TypeNode tn);
+
+ protected:
+ /** quant engine */
+ QuantifiersEngine* d_qe;
+ /** list of quantifiers asserted in the current context */
+ context::CDList<Node> d_forall_asserts;
+ /** quantified formulas marked as relevant */
+ unsigned d_rlv_count;
+ std::map<Node, unsigned> d_forall_rlv;
+ std::vector<Node> d_forall_rlv_vec;
+ Node d_last_forall_rlv;
+ std::vector<Node> d_forall_rlv_assert;
+ /** get variable id */
+ std::map<Node, std::map<Node, int> > d_quant_var_id;
+ /** process initialize model for term */
+ virtual void processInitializeModelForTerm(Node n) = 0;
+ /** process intialize quantifier */
+ virtual void processInitializeQuantifier(Node q) {}
+ /** process initialize */
+ virtual void processInitialize(bool ispre) = 0;
+
+ private:
+ // list of inactive quantified formulas
+ std::map<TNode, bool> d_quant_active;
+ /** map from types to model basis terms */
+ std::map<TypeNode, Node> d_model_basis_term;
+ /** 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 */
+ 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 */
+ void computeModelBasisArgAttribute(Node n);
};/* class FirstOrderModel */
bool isStar(Node n);
Node getStar(TypeNode tn);
Node getStarElement(TypeNode tn);
- bool isModelBasisTerm(Node n);
- Node getModelBasisTerm(TypeNode tn);
bool isInterval(Node n);
Node getInterval( Node lb, Node ub );
bool isInRange( Node v, Node i );
Trace("fmc-model-debug") << std::endl;
//possibly get default
if( needsDefault ){
- Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+ Node nmb = fm->getModelBasisOpTerm(op);
//add default value if necessary
if( fm->hasTerm( nmb ) ){
Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
ModelBasisArgSort mbas;
for (int i=0; i<(int)conds.size(); i++) {
mbas.d_terms.push_back(conds[i]);
- mbas.d_mba_count[conds[i]] =
- d_qe->getTermDatabase()->getModelBasisArg(conds[i]);
+ mbas.d_mba_count[conds[i]] = fm->getModelBasisArg(conds[i]);
indices.push_back(i);
}
std::sort( indices.begin(), indices.end(), mbas );
void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){
if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){
d_preinitialized_types[tn] = true;
- Node mb = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+ Node mb = fm->getModelBasisTerm(tn);
if( !mb.isConst() ){
Trace("fmc") << "...add model basis term to EE of model " << mb << " " << tn << std::endl;
fm->d_equalityEngine->addTerm( mb );
if( options::quantFunWellDefined() ){
Node hd = QuantAttributes::getFunDefHead( f );
if( !hd.isNull() ){
- hd = d_quantEngine->getTermUtil()->getInstConstantNode( hd, f );
+ hd = d_quantEngine->getTermUtil()
+ ->substituteBoundVariablesToInstConstants(hd, f);
patTermsF.push_back( hd );
tinfo[hd].init( f, hd );
}
if( tr ){
if( d_num_trigger_vars[q]<q[0].getNumChildren() ){
//partial trigger : generate implication to mark user pattern
- Node ipl = NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, d_quantEngine->getTermUtil()->getVariableNode( tr->getInstPattern(), q ) );
+ Node pat =
+ d_quantEngine->getTermUtil()->substituteInstConstantsToBoundVariables(
+ tr->getInstPattern(), q);
+ Node ipl = NodeManager::currentNM()->mkNode(INST_PATTERN_LIST, pat);
Node qq = NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[1][q], NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[0][q], q[1] ), ipl );
Trace("auto-gen-trigger-partial") << "Make partially specified user pattern: " << std::endl;
Trace("auto-gen-trigger-partial") << " " << qq << std::endl;
//}
//take into account user patterns
if( f.getNumChildren()==3 ){
- Node subsPat = d_quantEngine->getTermUtil()->getInstConstantNode( f[2], f );
+ Node subsPat =
+ d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants(
+ f[2], f);
//add patterns
for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
//Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
}
bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
- Node icn = d_qe->getTermUtil()->getInstConstantNode( n, f );
+ Node icn = d_qe->getTermUtil()->substituteBoundVariablesToInstConstants(n, f);
Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
std::vector< Node > var;
d_qe->getTermUtil()->getVarContainsNode( f, icn, var );
}
}
-
-
-bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
- if( argIndex<(int)n.getNumChildren() ){
+bool TermArgBasisTrie::addTerm(FirstOrderModel* fm, Node n, unsigned argIndex)
+{
+ if (argIndex < n.getNumChildren())
+ {
Node r;
if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){
r = n[ argIndex ];
}
std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r );
if( it==d_data.end() ){
- d_data[r].addTerm2( fm, n, argIndex+1 );
+ d_data[r].addTerm(fm, n, argIndex + 1);
return true;
}else{
- return it->second.addTerm2( fm, n, argIndex+1 );
+ return it->second.addTerm(fm, n, argIndex + 1);
}
}else{
return false;
for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node q = fm->getAssertedQuantifier( i );
if( d_qe->getModel()->isQuantifierActive( q ) ){
- int lems = initializeQuantifier( q, q );
+ int lems = initializeQuantifier(q, q, f);
d_statistics.d_init_inst_gen_lemmas += lems;
d_addedLemmas += lems;
if( d_qe->inConflict() ){
return TheoryEngineModelBuilder::processBuildModel( m );
}
-int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
+int QModelBuilderIG::initializeQuantifier(Node f, Node fp, FirstOrderModel* fm)
+{
if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){
//create the basis match if necessary
if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){
// }
//}
d_quant_basis_match[f] = InstMatch( f );
- for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
- Node t = d_qe->getTermDatabase()->getModelBasisTerm( f[0][j].getType() );
+ for (unsigned j = 0; j < f[0].getNumChildren(); j++)
+ {
+ Node t = fm->getModelBasisTerm(f[0][j].getType());
//calculate the basis match for f
d_quant_basis_match[f].setValue( j, t );
}
for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){
//the literal n is phase-required for quantifier f
Node n = it->first;
- Node gn = d_qe->getTermDatabase()->getModelBasis( f, n );
+ Node gn = fm->getModelBasis(f, n);
Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl;
bool value;
//if the corresponding ground abstraction literal has a SAT value
if( !d_uf_model_constructed[op] ){
//construct the model for the uninterpretted function/predicate
bool setDefaultVal = true;
- Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
+ Node defaultTerm = fmig->getModelBasisOpTerm(op);
Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl;
//set the values in the model
std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
if( defaultVal.isNull() ){
if (!fmig->getRepSet()->hasType(defaultTerm.getType()))
{
- Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(defaultTerm.getType());
+ Node mbt = fmig->getModelBasisTerm(defaultTerm.getType());
fmig->getRepSetPtr()->d_type_reps[defaultTerm.getType()].push_back(
mbt);
}
class TermArgBasisTrie {
-private:
- bool addTerm2( FirstOrderModel* fm, Node n, int argIndex );
public:
/** the data */
std::map< Node, TermArgBasisTrie > d_data;
-public:
- bool addTerm( FirstOrderModel* fm, Node n ) { return addTerm2( fm, n, 0 ); }
+ /** add term to the trie */
+ bool addTerm(FirstOrderModel* fm, Node n, unsigned argIndex = 0);
};/* class TermArgBasisTrie */
/** model builder class
//reset
virtual void reset( FirstOrderModel* fm ) = 0;
//initialize quantifiers, return number of lemmas produced
- virtual int initializeQuantifier( Node f, Node fp );
+ virtual int initializeQuantifier(Node f, Node fp, FirstOrderModel* fm);
//analyze model
virtual void analyzeModel( FirstOrderModel* fm );
//analyze quantifiers
Trace("model-engine-debug") << r << " ";
}
Trace("model-engine-debug") << std::endl;
- Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
+ Node mbt = fm->getModelBasisTerm(it->first);
Trace("model-engine-debug") << " Basis term : " << mbt << std::endl;
}
}
//check constraints
for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
//apply substitution to the tconstraint
- Node cons = p->getTermUtil()->getInstantiatedNode( it->first, d_q, terms );
+ Node cons =
+ p->getTermUtil()->substituteBoundVariables(it->first, d_q, terms);
cons = it->second ? cons : cons.negate();
if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){
return true;
#include "options/quantifiers_options.h"
#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/skolemize.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
Node sub;
std::vector< unsigned > sub_vars;
//return skolemized body
- return TermUtil::mkSkolemizedBody( n, nn, fvTypes, fvs, sk, sub, sub_vars );
+ return Skolemize::mkSkolemizedBody(
+ n, nn, fvTypes, fvs, sk, sub, sub_vars);
}
}else{
//check if it contains a quantifier as a subterm
Node RewriteEngine::getInstConstNode( Node n, Node q ) {
std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n );
if( it==d_inst_const_node[q].end() ){
- Node nn = d_quantEngine->getTermUtil()->getInstConstantNode( n, q );
+ Node nn =
+ d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants(
+ n, q);
d_inst_const_node[q][n] = nn;
return nn;
}else{
--- /dev/null
+/********************* */
+/*! \file skolemize.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 skolemization utility
+ **/
+
+#include "theory/quantifiers/skolemize.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/sort_inference.h"
+#include "theory/theory_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+Skolemize::Skolemize(QuantifiersEngine* qe, context::UserContext* u)
+ : d_quantEngine(qe), d_skolemized(u)
+{
+}
+
+Node Skolemize::process(Node q)
+{
+ // do skolemization
+ if (d_skolemized.find(q) == d_skolemized.end())
+ {
+ Node body = getSkolemizedBody(q);
+ NodeBuilder<> nb(kind::OR);
+ nb << q << body.notNode();
+ Node lem = nb;
+ d_skolemized[q] = lem;
+ return lem;
+ }
+ return Node::null();
+}
+
+bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems)
+{
+ std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it =
+ d_skolem_constants.find(q);
+ if (it != d_skolem_constants.end())
+ {
+ skolems.insert(skolems.end(), it->second.begin(), it->second.end());
+ return true;
+ }
+ return false;
+}
+
+Node Skolemize::getSkolemConstant(Node q, unsigned i)
+{
+ std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it =
+ d_skolem_constants.find(q);
+ if (it != d_skolem_constants.end())
+ {
+ if (i < it->second.size())
+ {
+ return it->second[i];
+ }
+ }
+ return Node::null();
+}
+
+void Skolemize::getSelfSel(const Datatype& dt,
+ const DatatypeConstructor& dc,
+ Node n,
+ TypeNode ntn,
+ std::vector<Node>& selfSel)
+{
+ TypeNode tspec;
+ if (dt.isParametric())
+ {
+ tspec = TypeNode::fromType(
+ dc.getSpecializedConstructorType(n.getType().toType()));
+ Trace("sk-ind-debug") << "Specialized constructor type : " << tspec
+ << std::endl;
+ Assert(tspec.getNumChildren() == dc.getNumArgs());
+ }
+ Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " "
+ << dt.getName() << std::endl;
+ for (unsigned j = 0; j < dc.getNumArgs(); j++)
+ {
+ std::vector<Node> ssc;
+ if (dt.isParametric())
+ {
+ Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn
+ << std::endl;
+ if (tspec[j] == ntn)
+ {
+ ssc.push_back(n);
+ }
+ }
+ else
+ {
+ TypeNode tn = TypeNode::fromType(dc[j].getRangeType());
+ Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
+ if (tn == ntn)
+ {
+ ssc.push_back(n);
+ }
+ }
+ /* TODO: more than weak structural induction
+ else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn
+ )==visited.end() ){
+ visited.push_back( tn );
+ const Datatype& dt =
+ ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
+ std::vector< Node > disj;
+ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+ getSelfSel( dt[i], n, ntn, ssc );
+ }
+ visited.pop_back();
+ }
+ */
+ for (unsigned k = 0; k < ssc.size(); k++)
+ {
+ Node ss = NodeManager::currentNM()->mkNode(
+ APPLY_SELECTOR_TOTAL,
+ dc.getSelectorInternal(n.getType().toType(), j),
+ n);
+ if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
+ {
+ selfSel.push_back(ss);
+ }
+ }
+ }
+}
+
+Node Skolemize::mkSkolemizedBody(Node f,
+ Node n,
+ std::vector<TypeNode>& argTypes,
+ std::vector<TNode>& fvs,
+ std::vector<Node>& sk,
+ Node& sub,
+ std::vector<unsigned>& sub_vars)
+{
+ Assert(sk.empty() || sk.size() == f[0].getNumChildren());
+ // calculate the variables and substitution
+ std::vector<TNode> ind_vars;
+ std::vector<unsigned> ind_var_indicies;
+ std::vector<TNode> vars;
+ std::vector<unsigned> var_indicies;
+ for (unsigned i = 0; i < f[0].getNumChildren(); i++)
+ {
+ if (isInductionTerm(f[0][i]))
+ {
+ ind_vars.push_back(f[0][i]);
+ ind_var_indicies.push_back(i);
+ }
+ else
+ {
+ vars.push_back(f[0][i]);
+ var_indicies.push_back(i);
+ }
+ Node s;
+ // make the new function symbol or use existing
+ if (i >= sk.size())
+ {
+ if (argTypes.empty())
+ {
+ s = NodeManager::currentNM()->mkSkolem(
+ "skv", f[0][i].getType(), "created during skolemization");
+ }
+ else
+ {
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType(
+ argTypes, f[0][i].getType());
+ Node op = NodeManager::currentNM()->mkSkolem(
+ "skop", typ, "op created during pre-skolemization");
+ // DOTHIS: set attribute on op, marking that it should not be selected
+ // as trigger
+ std::vector<Node> funcArgs;
+ funcArgs.push_back(op);
+ funcArgs.insert(funcArgs.end(), fvs.begin(), fvs.end());
+ s = NodeManager::currentNM()->mkNode(kind::APPLY_UF, funcArgs);
+ }
+ sk.push_back(s);
+ }
+ else
+ {
+ Assert(sk[i].getType() == f[0][i].getType());
+ }
+ }
+ Node ret;
+ if (vars.empty())
+ {
+ ret = n;
+ }
+ else
+ {
+ std::vector<Node> var_sk;
+ for (unsigned i = 0; i < var_indicies.size(); i++)
+ {
+ var_sk.push_back(sk[var_indicies[i]]);
+ }
+ Assert(vars.size() == var_sk.size());
+ ret = n.substitute(vars.begin(), vars.end(), var_sk.begin(), var_sk.end());
+ }
+ if (!ind_vars.empty())
+ {
+ Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
+ Trace("sk-ind") << "Skolemized is : " << ret << std::endl;
+ Node n_str_ind;
+ TypeNode tn = ind_vars[0].getType();
+ Node k = sk[ind_var_indicies[0]];
+ Node nret = ret.substitute(ind_vars[0], k);
+ // note : everything is under a negation
+ // the following constructs ~( R( x, k ) => ~P( x ) )
+ if (options::dtStcInduction() && tn.isDatatype())
+ {
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ std::vector<Node> disj;
+ for (unsigned i = 0; i < dt.getNumConstructors(); i++)
+ {
+ std::vector<Node> selfSel;
+ getSelfSel(dt, dt[i], k, tn, selfSel);
+ std::vector<Node> conj;
+ conj.push_back(
+ NodeManager::currentNM()
+ ->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), k)
+ .negate());
+ for (unsigned j = 0; j < selfSel.size(); j++)
+ {
+ conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate());
+ }
+ disj.push_back(conj.size() == 1
+ ? conj[0]
+ : NodeManager::currentNM()->mkNode(OR, conj));
+ }
+ Assert(!disj.empty());
+ n_str_ind = disj.size() == 1
+ ? disj[0]
+ : NodeManager::currentNM()->mkNode(AND, disj);
+ }
+ else if (options::intWfInduction() && tn.isInteger())
+ {
+ Node icond = NodeManager::currentNM()->mkNode(
+ GEQ, k, NodeManager::currentNM()->mkConst(Rational(0)));
+ Node iret =
+ ret.substitute(
+ ind_vars[0],
+ NodeManager::currentNM()->mkNode(
+ MINUS, k, NodeManager::currentNM()->mkConst(Rational(1))))
+ .negate();
+ n_str_ind = NodeManager::currentNM()->mkNode(OR, icond.negate(), iret);
+ n_str_ind = NodeManager::currentNM()->mkNode(AND, icond, n_str_ind);
+ }
+ else
+ {
+ Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0]
+ << ", type = " << tn << std::endl;
+ Assert(false);
+ }
+ Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl;
+
+ std::vector<Node> rem_ind_vars;
+ rem_ind_vars.insert(
+ rem_ind_vars.end(), ind_vars.begin() + 1, ind_vars.end());
+ if (!rem_ind_vars.empty())
+ {
+ Node bvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, rem_ind_vars);
+ nret = NodeManager::currentNM()->mkNode(FORALL, bvl, nret);
+ nret = Rewriter::rewrite(nret);
+ sub = nret;
+ sub_vars.insert(
+ sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end());
+ n_str_ind = NodeManager::currentNM()
+ ->mkNode(FORALL, bvl, n_str_ind.negate())
+ .negate();
+ }
+ ret = NodeManager::currentNM()->mkNode(OR, nret, n_str_ind);
+ }
+ Trace("quantifiers-sk-debug") << "mkSkolem body for " << f
+ << " returns : " << ret << std::endl;
+ // if it has an instantiation level, set the skolemized body to that level
+ if (f.hasAttribute(InstLevelAttribute()))
+ {
+ theory::QuantifiersEngine::setInstantiationLevelAttr(
+ ret, f.getAttribute(InstLevelAttribute()));
+ }
+
+ if (Trace.isOn("quantifiers-sk"))
+ {
+ Trace("quantifiers-sk") << "Skolemize : ";
+ for (unsigned i = 0; i < sk.size(); i++)
+ {
+ Trace("quantifiers-sk") << sk[i] << " ";
+ }
+ Trace("quantifiers-sk") << "for " << std::endl;
+ Trace("quantifiers-sk") << " " << f << std::endl;
+ }
+
+ return ret;
+}
+
+Node Skolemize::getSkolemizedBody(Node f)
+{
+ Assert(f.getKind() == FORALL);
+ if (d_skolem_body.find(f) == d_skolem_body.end())
+ {
+ std::vector<TypeNode> fvTypes;
+ std::vector<TNode> fvs;
+ Node sub;
+ std::vector<unsigned> sub_vars;
+ d_skolem_body[f] = mkSkolemizedBody(
+ f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars);
+ // store sub quantifier information
+ if (!sub.isNull())
+ {
+ // if we are skolemizing one at a time, we already know the skolem
+ // constants of the sub-quantified formula, store them
+ Assert(d_skolem_constants[sub].empty());
+ for (unsigned i = 0; i < sub_vars.size(); i++)
+ {
+ d_skolem_constants[sub].push_back(d_skolem_constants[f][sub_vars[i]]);
+ }
+ }
+ Assert(d_skolem_constants[f].size() == f[0].getNumChildren());
+ if (options::sortInference())
+ {
+ for (unsigned i = 0; i < d_skolem_constants[f].size(); i++)
+ {
+ // carry information for sort inference
+ d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar(
+ f, f[0][i], d_skolem_constants[f][i]);
+ }
+ }
+ }
+ return d_skolem_body[f];
+}
+
+bool Skolemize::isInductionTerm(Node n)
+{
+ TypeNode tn = n.getType();
+ if (options::dtStcInduction() && tn.isDatatype())
+ {
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ return !dt.isCodatatype();
+ }
+ if (options::intWfInduction() && n.getType().isInteger())
+ {
+ return true;
+ }
+ return false;
+}
+
+bool Skolemize::printSkolemization(std::ostream& out)
+{
+ bool printed = false;
+ for (NodeNodeMap::iterator it = d_skolemized.begin();
+ it != d_skolemized.end();
+ ++it)
+ {
+ Node q = (*it).first;
+ printed = true;
+ out << "(skolem " << q << std::endl;
+ out << " ( ";
+ for (unsigned i = 0; i < d_skolem_constants[q].size(); i++)
+ {
+ if (i > 0)
+ {
+ out << " ";
+ }
+ out << d_skolem_constants[q][i];
+ }
+ out << " )" << std::endl;
+ out << ")" << std::endl;
+ }
+ return printed;
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file skolemize.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 utilities for skolemization
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
+#define __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
+
+#include <unordered_map>
+#include <unordered_set>
+
+#include "context/cdhashmap.h"
+#include "expr/datatype.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers/quant_util.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Skolemization utility
+ *
+ * This class constructs Skolemization lemmas.
+ * Given a quantified formula q = (forall x. P),
+ * its skolemization lemma is of the form:
+ * (~ forall x. P ) => ~P * { x -> d_skolem_constants[q] }
+ *
+ * This class also incorporates techniques for
+ * skolemization with "inductive strenghtening", see
+ * Section 2 of Reynolds et al., "Induction for SMT
+ * Solvers", VMCAI 2015. In the case that x is an inductive
+ * datatype or an integer, then we may strengthen the conclusion
+ * based on weak well-founded induction. For example, for
+ * quantification on lists, a skolemization with inductive
+ * strengthening is a lemma of this form:
+ * (~ forall x : List. P( x ) ) =>
+ * ~P( k ) ^ ( is-cons( k ) => P( tail( k ) ) )
+ * For the integers it is:
+ * (~ forall x : Int. P( x ) ) =>
+ * ~P( k ) ^ ( x>0 => P( x-1 ) )
+ *
+ *
+ * Inductive strenghtening is not enabled by
+ * default and can be enabled by option:
+ * --quant-ind
+ */
+class Skolemize
+{
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+
+ public:
+ Skolemize(QuantifiersEngine* qe, context::UserContext* u);
+ ~Skolemize() {}
+ /** skolemize quantified formula q
+ * If the return value ret of this function
+ * is non-null, then ret is a new skolemization lemma
+ * we generated for q. These lemmas are constructed
+ * once per user-context.
+ */
+ Node process(Node q);
+ /** get skolem constants for quantified formula q */
+ bool getSkolemConstants(Node q, std::vector<Node>& skolems);
+ /** get the i^th skolem constant for quantified formula q */
+ Node getSkolemConstant(Node q, unsigned i);
+ /** make skolemized body
+ *
+ * This returns the skolemized body n of a
+ * quantified formula q with inductive strenghtening,
+ * where typically n is q[1].
+ *
+ * The skolem constants/functions we generate by this
+ * skolemization are added to sk.
+ *
+ * The arguments fvTypes and fvs are used if we are
+ * performing skolemization within a nested quantified
+ * formula. In this case, skolem constants we introduce
+ * must be parameterized based on fvTypes and must be
+ * applied to fvs.
+ *
+ * The last two arguments sub and sub_vars are used for
+ * to carry the body and indices of other induction
+ * variables if a quantified formula to skolemize
+ * has multiple induction variables. See page 5
+ * of Reynolds et al., VMCAI 2015.
+ */
+ static Node mkSkolemizedBody(Node q,
+ Node n,
+ std::vector<TypeNode>& fvTypes,
+ std::vector<TNode>& fvs,
+ std::vector<Node>& sk,
+ Node& sub,
+ std::vector<unsigned>& sub_vars);
+ /** get the skolemized body for quantified formula q */
+ Node getSkolemizedBody(Node q);
+ /** is n a variable that we can apply inductive strenghtening to? */
+ static bool isInductionTerm(Node n);
+ /** print all skolemizations
+ * This is used for the command line option
+ * --dump-instantiations
+ * which prints an informal justification
+ * of steps taken by the quantifiers module.
+ * Returns true if we printed at least one
+ * skolemization.
+ */
+ bool printSkolemization(std::ostream& out);
+
+ private:
+ /** get self selectors
+ * For datatype constructor dtc with type dt,
+ * this collects the set of datatype selector applications,
+ * applied to term n, whose return type in ntn, and stores
+ * them in the vector selfSel.
+ */
+ static void getSelfSel(const Datatype& dt,
+ const DatatypeConstructor& dc,
+ Node n,
+ TypeNode ntn,
+ std::vector<Node>& selfSel);
+ /** quantifiers engine that owns this module */
+ QuantifiersEngine* d_quantEngine;
+ /** quantified formulas that have been skolemized */
+ NodeNodeMap d_skolemized;
+ /** map from quantified formulas to the list of skolem constants */
+ std::unordered_map<Node, std::vector<Node>, NodeHashFunction>
+ d_skolem_constants;
+ /** map from quantified formulas to their skolemized body */
+ std::unordered_map<Node, Node, NodeHashFunction> d_skolem_body;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */
}
/** ground terms */
-unsigned TermDb::getNumGroundTerms( Node f ) {
- std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f );
+unsigned TermDb::getNumGroundTerms(Node f) const
+{
+ std::map<Node, std::vector<Node> >::const_iterator it = d_op_map.find(f);
if( it!=d_op_map.end() ){
return it->second.size();
}else{
}
}
-Node TermDb::getGroundTerm( Node f, unsigned i ) {
- Assert( i<d_op_map[f].size() );
- return d_op_map[f][i];
+Node TermDb::getGroundTerm(Node f, unsigned i) const
+{
+ std::map<Node, std::vector<Node> >::const_iterator it = d_op_map.find(f);
+ if (it != d_op_map.end())
+ {
+ Assert(i < it->second.size());
+ return it->second[i];
+ }
+ else
+ {
+ Assert(false);
+ return Node::null();
+ }
}
-unsigned TermDb::getNumTypeGroundTerms( TypeNode tn ) {
- std::map< TypeNode, std::vector< Node > >::iterator it = d_type_map.find( tn );
+unsigned TermDb::getNumTypeGroundTerms(TypeNode tn) const
+{
+ std::map<TypeNode, std::vector<Node> >::const_iterator it =
+ d_type_map.find(tn);
if( it!=d_type_map.end() ){
return it->second.size();
}else{
}
}
-Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) {
- Assert( i<d_type_map[tn].size() );
- return d_type_map[tn][i];
+Node TermDb::getTypeGroundTerm(TypeNode tn, unsigned i) const
+{
+ std::map<TypeNode, std::vector<Node> >::const_iterator it =
+ d_type_map.find(tn);
+ if (it != d_type_map.end())
+ {
+ Assert(i < it->second.size());
+ return it->second[i];
+ }
+ else
+ {
+ Assert(false);
+ return Node::null();
+ }
+}
+
+Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn)
+{
+ std::map<TypeNode, std::vector<Node> >::const_iterator it =
+ d_type_map.find(tn);
+ if (it != d_type_map.end())
+ {
+ Assert(!it->second.empty());
+ return it->second[0];
+ }
+ else
+ {
+ return getOrMakeTypeFreshVariable(tn);
+ }
+}
+
+Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
+{
+ std::unordered_map<TypeNode, Node, TypeNodeHashFunction>::iterator it =
+ d_type_fv.find(tn);
+ if (it == d_type_fv.end())
+ {
+ std::stringstream ss;
+ ss << language::SetLanguage(options::outputLanguage());
+ ss << "e_" << tn;
+ Node k = NodeManager::currentNM()->mkSkolem(
+ ss.str(), tn, "is a termDb fresh variable");
+ Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn
+ << std::endl;
+ if (options::instMaxLevel() != -1)
+ {
+ QuantifiersEngine::setInstantiationLevelAttr(k, 0);
+ }
+ d_type_fv[tn] = k;
+ return k;
+ }
+ else
+ {
+ return it->second;
+ }
}
Node TermDb::getMatchOperator( Node n ) {
//if this is an atomic trigger, consider adding it
if( inst::Trigger::isAtomicTrigger( n ) ){
Trace("term-db") << "register term in db " << n << std::endl;
- if( options::finiteModelFind() ){
- computeModelBasisArgAttribute( n );
- }
-
+
Node op = getMatchOperator( n );
Trace("term-db-debug") << " match operator is : " << op << std::endl;
d_ops.push_back(op);
return d_func_map_trie[f].existsTerm( args );
}
-
-Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
- if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
- Node mbt;
- if( tn.isInteger() || tn.isReal() ){
- mbt = NodeManager::currentNM()->mkConst(Rational(0));
- }else if( d_quantEngine->getTermUtil()->isClosedEnumerableType( tn ) ){
- mbt = tn.mkGroundTerm();
- }else{
- if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
- std::stringstream ss;
- ss << language::SetLanguage(options::outputLanguage());
- ss << "e_" << tn;
- mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
- Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
- if( options::instMaxLevel()!=-1 ){
- QuantifiersEngine::setInstantiationLevelAttr( mbt, 0 );
- }
- }else{
- mbt = d_type_map[ tn ][ 0 ];
- }
- }
- ModelBasisAttribute mba;
- mbt.setAttribute(mba,true);
- d_model_basis_term[tn] = mbt;
- Trace("model-basis-term") << "Choose " << mbt << " as model basis term for " << tn << std::endl;
- }
- return d_model_basis_term[tn];
-}
-
-Node TermDb::getModelBasisOpTerm( Node op ){
- if( d_model_basis_op_term.find( op )==d_model_basis_op_term.end() ){
- TypeNode t = op.getType();
- std::vector< Node > children;
- children.push_back( op );
- for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){
- children.push_back( getModelBasisTerm( t[i] ) );
- }
- if( children.size()==1 ){
- d_model_basis_op_term[op] = op;
- }else{
- d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children );
- }
- }
- return d_model_basis_op_term[op];
-}
-
-Node TermDb::getModelBasis( Node q, Node n ){
- //make model basis
- if( d_model_basis_terms.find( q )==d_model_basis_terms.end() ){
- for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
- d_model_basis_terms[q].push_back( getModelBasisTerm( q[0][j].getType() ) );
- }
- }
- Node gn = n.substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(),
- d_quantEngine->getTermUtil()->d_inst_constants[q].end(),
- d_model_basis_terms[q].begin(), d_model_basis_terms[q].end() );
- return gn;
-}
-
-Node TermDb::getModelBasisBody( Node q ){
- if( d_model_basis_body.find( q )==d_model_basis_body.end() ){
- Node n = d_quantEngine->getTermUtil()->getInstConstantBody( q );
- d_model_basis_body[q] = getModelBasis( q, n );
- }
- return d_model_basis_body[q];
-}
-
-void TermDb::computeModelBasisArgAttribute( Node n ){
- if( !n.hasAttribute(ModelBasisArgAttribute()) ){
- //ensure that the model basis terms have been defined
- if( n.getKind()==APPLY_UF ){
- getModelBasisOpTerm( n.getOperator() );
- }
- uint64_t val = 0;
- //determine if it has model basis attribute
- for( unsigned j=0; j<n.getNumChildren(); j++ ){
- if( n[j].getAttribute(ModelBasisAttribute()) ){
- val++;
- }
- }
- ModelBasisArgAttribute mbaa;
- n.setAttribute( mbaa, val );
- }
-}
-
-unsigned TermDb::getModelBasisArg(Node n)
-{
- computeModelBasisArgAttribute(n);
- return n.getAttribute(ModelBasisArgAttribute());
-}
-
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
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.
-*/
+ *
+ * This class is a key utility used by
+ * a number of approaches for quantifier instantiation,
+ * including E-matching, conflict-based instantiation,
+ * and model-based instantiation.
+ *
+ * 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.
+ *
+ * Like other utilities, its reset(...) function is called
+ * at the beginning of full or last call effort checks.
+ * This initializes the database for the round. However,
+ * notice that TermArgTrie objects are computed
+ * lazily for performance reasons.
+ */
class TermDb : public QuantifiersUtil {
friend class ::CVC4::theory::QuantifiersEngine;
// TODO: eliminate these
* Get the number of ground terms with operator f that have been added to the
* database
*/
- unsigned getNumGroundTerms(Node f);
+ unsigned getNumGroundTerms(Node f) const;
/** 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);
+ Node getGroundTerm(Node f, unsigned i) const;
/** get num type terms
* Get the number of ground terms of tn that have been added to the database
*/
- unsigned getNumTypeGroundTerms(TypeNode tn);
+ unsigned getNumTypeGroundTerms(TypeNode tn) const;
/** get type ground term
* Returns the i^th ground term of type tn
*/
- Node getTypeGroundTerm(TypeNode tn, unsigned i);
+ Node getTypeGroundTerm(TypeNode tn, unsigned i) const;
+ /** get or make ground term
+ * Returns the first ground term of type tn,
+ * or makes one if none exist.
+ */
+ Node getOrMakeTypeGroundTerm(TypeNode tn);
+ /** make fresh variable
+ * Returns a fresh variable of type tn.
+ * This will return only a single fresh
+ * variable per type.
+ */
+ Node getOrMakeTypeFreshVariable(TypeNode tn);
/** add a term to the database
* withinQuant is whether n is within the body of a quantified formula
* withinInstClosure is whether n is within an inst-closure operator (see
/** 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 )
+ * (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, 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
+ * (2) t is of the form f( t1, ..., tk ) where ti is in the
+ * equivalence class of args[i] 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.
+ * (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
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 */
+ /** get eligible term in equivalence class of r */
Node getEligibleTermInEqc(TNode r);
- /** is inst closure */
+ /** is r a inst closure node?
+ * This terminology was used for specifying
+ * a particular status of nodes for
+ * Bansal et al., CAV 2015.
+ */
bool isInstClosure(Node r);
private:
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;
+ /** map from type nodes to a fresh variable we introduced */
+ std::unordered_map<TypeNode, Node, TypeNodeHashFunction> d_type_fv;
/** inactive map */
NodeBoolMap d_inactive_map;
/** count of the number of non-redundant ground terms per operator */
/** get operator representative */
Node getOperatorRepresentative( TNode op ) const;
//------------------------------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 */
- std::map< Node, Node > d_model_basis_op_term;
- /** 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 */
- 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);
- /** get model basis arg */
- unsigned getModelBasisArg(Node n);
-
};/* class TermDb */
}/* CVC4::theory::quantifiers namespace */
--- /dev/null
+/********************* */
+/*! \file term_enumeration.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 term enumeration utility
+ **/
+
+#include "theory/quantifiers/term_enumeration.h"
+
+#include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index)
+{
+ Trace("term-db-enum") << "Get enumerate term " << tn << " " << index
+ << std::endl;
+ std::unordered_map<TypeNode, size_t, TypeNodeHashFunction>::iterator it =
+ d_typ_enum_map.find(tn);
+ size_t teIndex;
+ if (it == d_typ_enum_map.end())
+ {
+ teIndex = d_typ_enum.size();
+ d_typ_enum_map[tn] = teIndex;
+ d_typ_enum.push_back(TypeEnumerator(tn));
+ }
+ else
+ {
+ teIndex = it->second;
+ }
+ while (index >= d_enum_terms[tn].size())
+ {
+ if (d_typ_enum[teIndex].isFinished())
+ {
+ return Node::null();
+ }
+ d_enum_terms[tn].push_back(*d_typ_enum[teIndex]);
+ ++d_typ_enum[teIndex];
+ }
+ return d_enum_terms[tn][index];
+}
+
+bool TermEnumeration::isClosedEnumerableType(TypeNode tn)
+{
+ std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
+ d_typ_closed_enum.find(tn);
+ if (it == d_typ_closed_enum.end())
+ {
+ d_typ_closed_enum[tn] = true;
+ bool ret = true;
+ if (tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction())
+ {
+ ret = false;
+ }
+ else if (tn.isSet())
+ {
+ ret = isClosedEnumerableType(tn.getSetElementType());
+ }
+ else if (tn.isDatatype())
+ {
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ for (unsigned i = 0; i < dt.getNumConstructors(); i++)
+ {
+ for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
+ {
+ TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
+ if (tn != ctn && !isClosedEnumerableType(ctn))
+ {
+ ret = false;
+ break;
+ }
+ }
+ if (!ret)
+ {
+ break;
+ }
+ }
+ }
+
+ // other parametric sorts go here
+
+ d_typ_closed_enum[tn] = ret;
+ return ret;
+ }
+ else
+ {
+ return it->second;
+ }
+}
+
+// checks whether a type is closed enumerable and is reasonably small enough (<1000)
+// such that all of its domain elements can be enumerated
+bool TermEnumeration::mayComplete(TypeNode tn)
+{
+ std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
+ d_may_complete.find(tn);
+ if (it == d_may_complete.end())
+ {
+ bool mc = false;
+ if (isClosedEnumerableType(tn) && tn.getCardinality().isFinite()
+ && !tn.getCardinality().isLargeFinite())
+ {
+ Node card = NodeManager::currentNM()->mkConst(
+ Rational(tn.getCardinality().getFiniteCardinality()));
+ Node oth = NodeManager::currentNM()->mkConst(Rational(1000));
+ Node eq = NodeManager::currentNM()->mkNode(LEQ, card, oth);
+ eq = Rewriter::rewrite(eq);
+ mc = eq.isConst() && eq.getConst<bool>();
+ }
+ d_may_complete[tn] = mc;
+ return mc;
+ }
+ else
+ {
+ return it->second;
+ }
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file term_enumeration.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 utilities for term enumeration
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
+#define __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
+
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/type_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Term enumeration
+ *
+ * This class has utilities for enumerating terms. It stores
+ * a cache of terms enumerated per each type.
+ * It also has various utility functions regarding type
+ * enumeration.
+ */
+class TermEnumeration
+{
+ public:
+ TermEnumeration() {}
+ ~TermEnumeration() {}
+ /** get i^th term for type tn */
+ Node getEnumerateTerm(TypeNode tn, unsigned i);
+ /** is closed enumerable type
+ *
+ * This returns true if this type has an enumerator that produces
+ * constants that are handled by ground theory solvers.
+ * Examples of types that are not closed enumerable are:
+ * (1) uninterpreted sorts,
+ * (2) arrays,
+ * (3) codatatypes,
+ * (4) parametric sorts involving any of the above.
+ */
+ bool isClosedEnumerableType(TypeNode tn);
+ /** may complete type
+ *
+ * Returns true if the type tn is closed
+ * enumerable, and is small enough
+ * for finite model finding to enumerate it,
+ * by some heuristic (current cardinality < 1000).
+ */
+ bool mayComplete(TypeNode tn);
+
+ private:
+ /** ground terms enumerated for types */
+ std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>
+ d_enum_terms;
+ /** map from type to the index of its type enumerator in d_typ_enum. */
+ std::unordered_map<TypeNode, size_t, TypeNodeHashFunction> d_typ_enum_map;
+ /** type enumerators */
+ std::vector<TypeEnumerator> d_typ_enum;
+ /** closed enumerable type cache */
+ std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_typ_closed_enum;
+ /** may complete */
+ std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_may_complete;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */
#include "expr/datatype.h"
#include "options/base_options.h"
-#include "options/quantifiers_options.h"
#include "options/datatypes_options.h"
+#include "options/quantifiers_options.h"
#include "options/uf_options.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
using namespace std;
using namespace CVC4::kind;
Node TermUtil::getInstConstantBody( Node q ){
std::map< Node, Node >::iterator it = d_inst_const_body.find( q );
if( it==d_inst_const_body.end() ){
- Node n = getInstConstantNode( q[1], q );
+ Node n = substituteBoundVariablesToInstConstants(q[1], q);
d_inst_const_body[ q ] = n;
return n;
}else{
return d_ce_lit[ q ];
}
-Node TermUtil::getInstConstantNode( Node n, Node q ){
+Node TermUtil::substituteBoundVariablesToInstConstants(Node n, Node q)
+{
registerQuantifier( q );
return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() );
}
-Node TermUtil::getVariableNode( Node n, Node q ) {
+Node TermUtil::substituteInstConstantsToBoundVariables(Node n, Node q)
+{
registerQuantifier( q );
return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() );
}
-Node TermUtil::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) {
+Node TermUtil::substituteBoundVariables(Node n,
+ Node q,
+ std::vector<Node>& terms)
+{
+ registerQuantifier(q);
Assert( d_vars[q].size()==terms.size() );
return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() );
}
-
-void getSelfSel( const Datatype& dt, const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
- TypeNode tspec;
- if( dt.isParametric() ){
- tspec = TypeNode::fromType( dc.getSpecializedConstructorType(n.getType().toType()) );
- Trace("sk-ind-debug") << "Specialized constructor type : " << tspec << std::endl;
- Assert( tspec.getNumChildren()==dc.getNumArgs() );
- }
- Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " " << dt.getName() << std::endl;
- for( unsigned j=0; j<dc.getNumArgs(); j++ ){
- std::vector< Node > ssc;
- if( dt.isParametric() ){
- Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn << std::endl;
- if( tspec[j]==ntn ){
- ssc.push_back( n );
- }
- }else{
- TypeNode tn = TypeNode::fromType( dc[j].getRangeType() );
- Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
- if( tn==ntn ){
- ssc.push_back( n );
- }
- }
- /* TODO: more than weak structural induction
- else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn )==visited.end() ){
- visited.push_back( tn );
- const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
- std::vector< Node > disj;
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- getSelfSel( dt[i], n, ntn, ssc );
- }
- visited.pop_back();
- }
- */
- for( unsigned k=0; k<ssc.size(); k++ ){
- Node ss = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, dc.getSelectorInternal( n.getType().toType(), j ), n );
- if( std::find( selfSel.begin(), selfSel.end(), ss )==selfSel.end() ){
- selfSel.push_back( ss );
- }
- }
- }
-}
-
-
-Node TermUtil::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes, std::vector< TNode >& fvs,
- std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ) {
- Assert( sk.empty() || sk.size()==f[0].getNumChildren() );
- //calculate the variables and substitution
- std::vector< TNode > ind_vars;
- std::vector< unsigned > ind_var_indicies;
- std::vector< TNode > vars;
- std::vector< unsigned > var_indicies;
- for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
- if( isInductionTerm( f[0][i] ) ){
- ind_vars.push_back( f[0][i] );
- ind_var_indicies.push_back( i );
- }else{
- vars.push_back( f[0][i] );
- var_indicies.push_back( i );
- }
- Node s;
- //make the new function symbol or use existing
- if( i>=sk.size() ){
- if( argTypes.empty() ){
- s = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "created during skolemization" );
- }else{
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, f[0][i].getType() );
- Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" );
- //DOTHIS: set attribute on op, marking that it should not be selected as trigger
- std::vector< Node > funcArgs;
- funcArgs.push_back( op );
- funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
- s = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
- }
- sk.push_back( s );
- }else{
- Assert( sk[i].getType()==f[0][i].getType() );
- }
- }
- Node ret;
- if( vars.empty() ){
- ret = n;
- }else{
- std::vector< Node > var_sk;
- for( unsigned i=0; i<var_indicies.size(); i++ ){
- var_sk.push_back( sk[var_indicies[i]] );
- }
- Assert( vars.size()==var_sk.size() );
- ret = n.substitute( vars.begin(), vars.end(), var_sk.begin(), var_sk.end() );
- }
- if( !ind_vars.empty() ){
- Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
- Trace("sk-ind") << "Skolemized is : " << ret << std::endl;
- Node n_str_ind;
- TypeNode tn = ind_vars[0].getType();
- Node k = sk[ind_var_indicies[0]];
- Node nret = ret.substitute( ind_vars[0], k );
- //note : everything is under a negation
- //the following constructs ~( R( x, k ) => ~P( x ) )
- if( options::dtStcInduction() && tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- std::vector< Node > disj;
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- std::vector< Node > selfSel;
- getSelfSel( dt, dt[i], k, tn, selfSel );
- std::vector< Node > conj;
- conj.push_back( NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), k ).negate() );
- for( unsigned j=0; j<selfSel.size(); j++ ){
- conj.push_back( ret.substitute( ind_vars[0], selfSel[j] ).negate() );
- }
- disj.push_back( conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( OR, conj ) );
- }
- Assert( !disj.empty() );
- n_str_ind = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( AND, disj );
- }else if( options::intWfInduction() && tn.isInteger() ){
- Node icond = NodeManager::currentNM()->mkNode( GEQ, k, NodeManager::currentNM()->mkConst( Rational(0) ) );
- Node iret = ret.substitute( ind_vars[0], NodeManager::currentNM()->mkNode( MINUS, k, NodeManager::currentNM()->mkConst( Rational(1) ) ) ).negate();
- n_str_ind = NodeManager::currentNM()->mkNode( OR, icond.negate(), iret );
- n_str_ind = NodeManager::currentNM()->mkNode( AND, icond, n_str_ind );
- }else{
- Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0] << ", type = " << tn << std::endl;
- Assert( false );
- }
- Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl;
-
- std::vector< Node > rem_ind_vars;
- rem_ind_vars.insert( rem_ind_vars.end(), ind_vars.begin()+1, ind_vars.end() );
- if( !rem_ind_vars.empty() ){
- Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, rem_ind_vars );
- nret = NodeManager::currentNM()->mkNode( FORALL, bvl, nret );
- nret = Rewriter::rewrite( nret );
- sub = nret;
- sub_vars.insert( sub_vars.end(), ind_var_indicies.begin()+1, ind_var_indicies.end() );
- n_str_ind = NodeManager::currentNM()->mkNode( FORALL, bvl, n_str_ind.negate() ).negate();
- }
- ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind );
- }
- Trace("quantifiers-sk-debug") << "mkSkolem body for " << f << " returns : " << ret << std::endl;
- //if it has an instantiation level, set the skolemized body to that level
- if( f.hasAttribute(InstLevelAttribute()) ){
- theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) );
- }
-
- if( Trace.isOn("quantifiers-sk") ){
- Trace("quantifiers-sk") << "Skolemize : ";
- for( unsigned i=0; i<sk.size(); i++ ){
- Trace("quantifiers-sk") << sk[i] << " ";
- }
- Trace("quantifiers-sk") << "for " << std::endl;
- Trace("quantifiers-sk") << " " << f << std::endl;
- }
-
- return ret;
-}
-
-Node TermUtil::getSkolemizedBody( Node f ){
- Assert( f.getKind()==FORALL );
- if( d_skolem_body.find( f )==d_skolem_body.end() ){
- std::vector< TypeNode > fvTypes;
- std::vector< TNode > fvs;
- Node sub;
- std::vector< unsigned > sub_vars;
- d_skolem_body[ f ] = mkSkolemizedBody( f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars );
- //store sub quantifier information
- if( !sub.isNull() ){
- //if we are skolemizing one at a time, we already know the skolem constants of the sub-quantified formula, store them
- Assert( d_skolem_constants[sub].empty() );
- for( unsigned i=0; i<sub_vars.size(); i++ ){
- d_skolem_constants[sub].push_back( d_skolem_constants[f][sub_vars[i]] );
- }
- }
- Assert( d_skolem_constants[f].size()==f[0].getNumChildren() );
- if( options::sortInference() ){
- for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){
- //carry information for sort inference
- d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] );
- }
- }
- }
- return d_skolem_body[ f ];
-}
-
-Node TermUtil::getEnumerateTerm( TypeNode tn, unsigned index ) {
- Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl;
- std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn );
- unsigned teIndex;
- if( it==d_typ_enum_map.end() ){
- teIndex = (int)d_typ_enum.size();
- d_typ_enum_map[tn] = teIndex;
- d_typ_enum.push_back( TypeEnumerator(tn) );
- }else{
- teIndex = it->second;
- }
- while( index>=d_enum_terms[tn].size() ){
- if( d_typ_enum[teIndex].isFinished() ){
- return Node::null();
- }
- d_enum_terms[tn].push_back( *d_typ_enum[teIndex] );
- ++d_typ_enum[teIndex];
- }
- return d_enum_terms[tn][index];
-}
-
-bool TermUtil::isClosedEnumerableType( TypeNode tn ) {
- std::map< TypeNode, bool >::iterator it = d_typ_closed_enum.find( tn );
- if( it==d_typ_closed_enum.end() ){
- d_typ_closed_enum[tn] = true;
- bool ret = true;
- if( tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction() ){
- ret = false;
- }else if( tn.isSet() ){
- ret = isClosedEnumerableType( tn.getSetElementType() );
- }else if( tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
- TypeNode ctn = TypeNode::fromType( dt[i][j].getRangeType() );
- if( tn!=ctn && !isClosedEnumerableType( ctn ) ){
- ret = false;
- break;
- }
- }
- if( !ret ){
- break;
- }
- }
- }
- //TODO: other parametric sorts go here
- d_typ_closed_enum[tn] = ret;
- return ret;
- }else{
- return it->second;
- }
-}
-
-//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated
-bool TermUtil::mayComplete( TypeNode tn ) {
- std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn );
- if( it==d_may_complete.end() ){
- bool mc = false;
- if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){
- Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) );
- Node oth = NodeManager::currentNM()->mkConst( Rational(1000) );
- Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth );
- eq = Rewriter::rewrite( eq );
- mc = eq==d_true;
- }
- d_may_complete[tn] = mc;
- return mc;
- }else{
- return it->second;
- }
+Node TermUtil::substituteInstConstants(Node n, Node q, std::vector<Node>& terms)
+{
+ registerQuantifier(q);
+ Assert(d_inst_constants[q].size() == terms.size());
+ return n.substitute(d_inst_constants[q].begin(),
+ d_inst_constants[q].end(),
+ terms.begin(),
+ terms.end());
}
void TermUtil::computeVarContains( Node n, std::vector< Node >& varContains ) {
( n.getKind()!=ITE || n.getType().isBoolean() );
}
-void TermUtil::registerTrigger( theory::inst::Trigger* tr, Node op ){
- if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
- d_op_triggers[op].push_back( tr );
- }
-}
-
Node TermUtil::getHoTypeMatchPredicate( TypeNode tn ) {
std::map< TypeNode, Node >::iterator ithp = d_ho_type_match_pred.find( tn );
if( ithp==d_ho_type_match_pred.end() ){
}
}
-bool TermUtil::isInductionTerm( Node n ) {
- TypeNode tn = n.getType();
- if( options::dtStcInduction() && tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- return !dt.isCodatatype();
- }
- if( options::intWfInduction() && n.getType().isInteger() ){
- return true;
- }
- return false;
-}
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
struct ContainsUConstAttributeId {};
typedef expr::Attribute<ContainsUConstAttributeId, uint64_t> ContainsUConstAttribute;
-struct ModelBasisAttributeId {};
-typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
-//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
-// 0 : term has no direct child with model basis attribute.
-struct ModelBasisArgAttributeId {};
-typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
-
//for bounded integers
struct BoundIntLitAttributeId {};
typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute;
struct LtePartialInstAttributeId {};
typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute;
-// attribute for "contains instantiation constants from"
+// attribute for sygus proxy variables
struct SygusProxyAttributeId {};
typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute;
{
// TODO : remove these
friend class ::CVC4::theory::QuantifiersEngine;
- friend class TermDatabase;
private:
/** reference to the quantifiers engine */
QuantifiersEngine* d_quantEngine;
return a pattern where the variable are replaced by variable for
instantiation.
*/
- Node getInstConstantNode( Node n, Node q );
- Node getVariableNode( Node n, Node q );
- /** get substituted node */
- Node getInstantiatedNode( Node n, Node q, std::vector< Node >& terms );
+ Node substituteBoundVariablesToInstConstants(Node n, Node q);
+ /** substitute { instantiation constants of q -> bound variables of q } in n
+ */
+ Node substituteInstConstantsToBoundVariables(Node n, Node q);
+ /** substitute { variables of q -> terms } in n */
+ Node substituteBoundVariables(Node n, Node q, std::vector<Node>& terms);
+ /** substitute { instantiation constants of q -> terms } in n */
+ Node substituteInstConstants(Node n, Node q, std::vector<Node>& terms);
static Node getInstConstAttr( Node n );
static bool hasInstConstAttr( Node n );
//quantified simplify (treat free variables in n as quantified and run rewriter)
static Node getQuantSimplify( Node n );
-//for skolem
-private:
- /** map from universal quantifiers to their skolemized body */
- std::map< Node, Node > d_skolem_body;
-public:
- /** map from universal quantifiers to the list of skolem constants */
- std::map< Node, std::vector< Node > > d_skolem_constants;
- /** make the skolemized body f[e/x] */
- static Node mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs,
- std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars );
- /** get the skolemized body */
- Node getSkolemizedBody( Node f);
- /** is induction variable */
- static bool isInductionTerm( Node n );
-
-//for ground term enumeration
-private:
- /** ground terms enumerated for types */
- std::map< TypeNode, std::vector< Node > > d_enum_terms;
- //type enumerators
- std::map< TypeNode, unsigned > d_typ_enum_map;
- std::vector< TypeEnumerator > d_typ_enum;
- // closed enumerable type cache
- std::map< TypeNode, bool > d_typ_closed_enum;
- /** may complete */
- std::map< TypeNode, bool > d_may_complete;
-public:
- //get nth term for type
- Node getEnumerateTerm( TypeNode tn, unsigned index );
- //does this type have an enumerator that produces constants that are handled by ground theory solvers
- bool isClosedEnumerableType( TypeNode tn );
- // may complete
- bool mayComplete( TypeNode tn );
-
//for triggers
private:
/** helper function for compute var contains */
static void computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited );
- /** triggers for each operator */
- std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
/** helper for is instance of */
static bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
/** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
static int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 );
-public:
+ /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
+ static int isInstanceOf(Node n1, Node n2);
+
+ public:
/** compute var contains */
static void computeVarContains( Node n, std::vector< Node >& varContains );
/** get var contains for each of the patterns in pats */
static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
/** compute quant contains */
static void computeQuantContains( Node n, std::vector< Node >& quantContains );
- /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
- static int isInstanceOf( Node n1, Node n2 );
+ // TODO (#1216) : this should be in trigger.h
/** filter all nodes that have instances */
static void filterInstances( std::vector< Node >& nodes );
- /** register trigger (for eager quantifier instantiation) */
- void registerTrigger( inst::Trigger* tr, Node op );
//for term ordering
private:
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/relevant_domain.h"
#include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/skolemize.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/sep/theory_sep.h"
TheoryEngine* te)
: d_te(te),
d_quant_attr(new quantifiers::QuantAttributes(this)),
+ d_skolemize(new quantifiers::Skolemize(this, u)),
+ d_term_enum(new quantifiers::TermEnumeration),
d_conflict_c(c, false),
// d_quants(u),
d_quants_red(u),
d_lemmas_produced_c(u),
- d_skolemized(u),
d_ierCounter_c(c),
// d_ierCounter(c),
// d_ierCounter_lc(c),
TypeNode tn = v.getType();
if( tn.isSort() && options::finiteModelFind() ){
return true;
- }else if( getTermUtil()->mayComplete( tn ) ){
+ }
+ else if (d_term_enum->mayComplete(tn))
+ {
return true;
}
}
//if not reduced
if( !reduceQuantifier( f ) ){
//do skolemization
- if( d_skolemized.find( f )==d_skolemized.end() ){
- Node body = d_term_util->getSkolemizedBody( f );
- NodeBuilder<> nb(kind::OR);
- nb << f << body.notNode();
- Node lem = nb;
+ Node lem = d_skolemize->process(f);
+ if (!lem.isNull())
+ {
if( Trace.isOn("quantifiers-sk-debug") ){
Node slem = Rewriter::rewrite( lem );
Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl;
}
getOutputChannel().lemma( lem, false, true );
- d_skolemized[f] = true;
}
}
}else{
//only wait if we are doing incremental solving
if( !d_presolve || !options::incrementalSolving() ){
std::set< Node > added;
- getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
-
+ d_term_db->addTerm(n, added, withinQuant, withinInstClosure);
+
//added contains also the Node that just have been asserted in this branch
if( d_quant_rel ){
for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
for( unsigned i=0; i<terms.size(); i++ ){
Trace("inst-add-debug") << " " << q[0][i];
Trace("inst-add-debug2") << " -> " << terms[i];
+ TypeNode tn = q[0][i].getType();
if( terms[i].isNull() ){
- terms[i] = d_term_db->getModelBasisTerm( q[0][i].getType() );
+ terms[i] = getTermForType(tn);
}
if( mkRep ){
//pick the best possible representative for instantiation, based on past use and simplicity of term
terms[i] = getInternalRepresentative( terms[i], q, i );
}else{
//ensure the type is correct
- terms[i] = quantifiers::TermUtil::ensureType( terms[i], q[0][i].getType() );
+ terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn);
}
Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
if( terms[i].isNull() ){
}
bool printed = false;
- for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){
- Node q = (*it).first;
+ // print the skolemizations
+ if (d_skolemize->printSkolemization(out))
+ {
printed = true;
- out << "(skolem " << q << std::endl;
- out << " ( ";
- for( unsigned i=0; i<d_term_util->d_skolem_constants[q].size(); i++ ){
- if( i>0 ){ out << " "; }
- out << d_term_util->d_skolem_constants[q][i];
- }
- out << " )" << std::endl;
- out << ")" << std::endl;
}
+ // print the instantiations
if( options::incrementalSolving() ){
for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
bool firstTime = true;
return ret;
}
+Node QuantifiersEngine::getTermForType(TypeNode tn)
+{
+ if (d_term_enum->isClosedEnumerableType(tn))
+ {
+ return d_term_enum->getEnumerateTerm(tn, 0);
+ }
+ else
+ {
+ return d_term_db->getOrMakeTypeGroundTerm(tn);
+ }
+}
+
void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
eq::EqualityEngine* ee = getActiveEqualityEngine();
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
namespace quantifiers {
//TODO: organize this more/review this, github issue #1163
+ //TODO: include these instead of doing forward declarations? #1307
//utilities
class TermDb;
class TermDbSygus;
class TermUtil;
+ class Skolemize;
+ class TermEnumeration;
class FirstOrderModel;
class QuantAttributes;
class RelevantDomain;
quantifiers::TermUtil* d_term_util;
/** quantifiers attributes */
std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
+ /** skolemize utility */
+ std::unique_ptr<quantifiers::Skolemize> d_skolemize;
+ /** term enumeration utility */
+ std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
private:
/** instantiation engine */
std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
/** recorded instantiations */
std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst;
- /** quantifiers that have been skolemized */
- BoolMap d_skolemized;
/** all triggers will be stored in this trie */
inst::TriggerTrie* d_tr_trie;
/** extended model object */
quantifiers::QuantAttributes* getQuantAttributes() {
return d_quant_attr.get();
}
+ /** get skolemize utility */
+ quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); }
+ /** get term enumeration utility */
+ quantifiers::TermEnumeration* getTermEnumeration()
+ {
+ return d_term_enum.get();
+ }
/** get trigger database */
inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
/** add term to database */
void debugPrintEqualityEngine( const char * c );
/** get internal representative */
Node getInternalRepresentative( Node a, Node q, int index );
-public:
+ /** get term for type
+ *
+ * This returns an arbitrary term for type tn.
+ * This term is chosen heuristically to be the best
+ * term for instantiation. Currently, this
+ * heuristic enumerates the first term of the
+ * type if the type is closed enumerable, otherwise
+ * an existing ground term from the term database if
+ * one exists, or otherwise a fresh variable.
+ */
+ Node getTermForType(TypeNode tn);
+
+ public:
/** print instantiations */
void printInstantiations( std::ostream& out );
/** print solution for synthesis conjectures */
#include <unordered_set>
-#include "theory/rep_set.h"
-#include "theory/type_enumerator.h"
#include "theory/quantifiers/bounded_integers.h"
-#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/rep_set.h"
+#include "theory/type_enumerator.h"
using namespace std;
using namespace CVC4;
return initialize( rext );
}
+// TODO : as part of #1199, the portions of this
+// function which modify d_rep_set should be
+// moved to TheoryModel.
bool RepSetIterator::initialize( RepBoundExt* rext ){
Trace("rsi") << "Initialize rep set iterator..." << std::endl;
for( unsigned v=0; v<d_types.size(); v++ ){
}
if( !tn.isSort() ){
if( inc ){
- if( d_qe->getTermUtil()->mayComplete( tn ) ){
+ if (d_qe->getTermEnumeration()->mayComplete(tn))
+ {
Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
d_rep_set->complete( tn );
//must have succeeded
#include "expr/attribute.h"
#include "options/quantifiers_options.h"
-#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/first_order_model.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
namespace theory {
namespace uf {
+// TODO (#1302) : some of these classes should be moved to
+// src/theory/quantifiers/
class UfModelTreeNode
{
public:
projects / cvc5.git / commitdiff