diff options
Diffstat (limited to 'src/theory/quantifiers/ceg_instantiator.h')
| -rw-r--r-- | src/theory/quantifiers/ceg_instantiator.h | 643 |
1 files changed, 465 insertions, 178 deletions
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 1e59bfb43..bf5a37026 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -39,10 +39,14 @@ public: }; class Instantiator; +class InstantiatorPreprocess; /** Term Properties - * stores properties for a variable to solve for in CEGQI - * For LIA, this includes the coefficient of the variable, and the bound type + * + * Stores properties for a variable to solve for in counterexample-guided + * instantiation. + * + * For LIA, this includes the coefficient of the variable, and the bound type * for the variable. */ class TermProperties { @@ -53,8 +57,9 @@ public: int d_type; // for arithmetic Node d_coeff; - // get cache node - // we consider terms + TermProperties that are unique up to their cache node (see doAddInstantiationInc) + // get cache node + // we consider terms + TermProperties that are unique up to their cache node + // (see constructInstantiationInc) virtual Node getCacheNode() const { return d_coeff; } // is non-basic virtual bool isBasic() const { return d_coeff.isNull(); } @@ -138,12 +143,126 @@ public: } }; +/** instantiation effort levels */ +enum InstEffort +{ + // uninitialized + INST_EFFORT_NONE, + // standard effort level + INST_EFFORT_STANDARD, + // standard effort level, but we have used model values + INST_EFFORT_STANDARD_MV, + // full effort level + INST_EFFORT_FULL +}; + /** Ceg instantiator * * This class manages counterexample-guided quantifier instantiation * for a single quantified formula. + * + * For details on counterexample-guided quantifier instantiation + * (for linear arithmetic), see Reynolds/King/Kuncak FMSD 2017. */ class CegInstantiator { + public: + CegInstantiator(QuantifiersEngine* qe, + CegqiOutput* out, + bool use_vts_delta = true, + bool use_vts_inf = true); + virtual ~CegInstantiator(); + /** check + * This adds instantiations based on the state of d_vars in current context + * on the output channel d_out of this class. + */ + bool check(); + /** presolve for quantified formula + * + * This initializes formulas that help static learning of the quantifier-free + * solver. It is only called if the option --cbqi-prereg-inst is used. + */ + void presolve(Node q); + /** Register the counterexample lemma + * + * lems : contains the conjuncts of the counterexample lemma of the + * quantified formula we are processing. The counterexample + * lemma is the formula { ~phi[e/x] } in Figure 1 of Reynolds + * et al. FMSD 2017. + * ce_vars : contains the variables e. Notice these are variables of + * INST_CONSTANT kind, since we do not permit bound + * variables in assertions. + * + * This method may modify the set of lemmas lems based on: + * - ITE removal, + * - Theory-specific preprocessing of instantiation lemmas. + * It may also introduce new variables to ce_vars if necessary. + */ + void registerCounterexampleLemma(std::vector<Node>& lems, + std::vector<Node>& ce_vars); + /** get the output channel of this class */ + CegqiOutput* getOutput() { return d_out; } + //------------------------------interface for instantiators + /** get quantifiers engine */ + QuantifiersEngine* getQuantifiersEngine() { return d_qe; } + /** push stack variable + * This adds a new variable to solve for in the stack + * of variables we are processing. This stack is only + * used for datatypes, where e.g. the DtInstantiator + * solving for a list x may push the stack "variables" + * head(x) and tail(x). + */ + void pushStackVariable(Node v); + /** pop stack variable */ + void popStackVariable(); + /** construct instantiation increment + * + * Adds the substitution { pv_prop.getModifiedTerm(pv) -> n } to the current + * instantiation, specified by sf. + * + * This function returns true if a call to + * QuantifiersEngine::addInstantiation(...) + * was successfully made in a recursive call. + * + * The solved form sf is reverted to its original state if + * this function returns false, or + * revertOnSuccess is true and this function returns true. + */ + bool constructInstantiationInc(Node pv, + Node n, + TermProperties& pv_prop, + SolvedForm& sf, + bool revertOnSuccess = false); + /** get the current model value of term n */ + Node getModelValue(Node n); + /** get bound variable for type + * + * This gets the next (canonical) bound variable of + * type tn. This can be used for instance when + * constructing instantiations that involve choice expressions. + */ + Node getBoundVariable(TypeNode tn); + //------------------------------end interface for instantiators + + /** + * Get the number of atoms in the counterexample lemma of the quantified + * formula we are processing with this class. + */ + unsigned getNumCEAtoms() { return d_ce_atoms.size(); } + /** + * Get the i^th atom of the counterexample lemma of the quantified + * formula we are processing with this class. + */ + Node getCEAtom(unsigned i) { return d_ce_atoms[i]; } + /** is n a term that is eligible for instantiation? */ + bool isEligible(Node n); + /** does n have variable pv? */ + bool hasVariable(Node n, Node pv); + /** are we using delta for LRA virtual term substitution? */ + bool useVtsDelta() { return d_use_vts_delta; } + /** are we using infinity for LRA virtual term substitution? */ + bool useVtsInfinity() { return d_use_vts_inf; } + /** are we processing a nested quantified formula? */ + bool hasNestedQuantification() { return d_is_nested_quant; } private: /** quantified formula associated with this instantiator */ QuantifiersEngine* d_qe; @@ -157,6 +276,8 @@ class CegInstantiator { * (for quantified LRA). */ bool d_use_vts_inf; + + //-------------------------------globally cached /** cache from nodes to the set of variables it contains * (from the quantified formula we are instantiating). */ @@ -168,25 +289,88 @@ class CegInstantiator { * ineligible for instantiation. */ std::unordered_set<Node, NodeHashFunction> d_inelig; + /** ensures n is in d_prog_var and d_inelig. */ + void computeProgVars(Node n); + //-------------------------------end globally cached + + //-------------------------------cached per round /** current assertions per theory */ std::map<TheoryId, std::vector<Node> > d_curr_asserts; /** map from representatives to the terms in their equivalence class */ std::map<Node, std::vector<Node> > d_curr_eqc; /** map from types to representatives of that type */ std::map<TypeNode, std::vector<Node> > d_curr_type_eqc; - /** auxiliary variables - * These variables include the result of removing ITE - * terms from the quantified formula we are processing. - * These variables must be eliminated from constraints - * as a preprocess step to check(). + /** process assertions + * This is called once at the beginning of check to + * set up all necessary information for constructing instantiations, + * such as the above data structures. */ - std::vector<Node> d_aux_vars; + void processAssertions(); + /** add to auxiliary variable substitution + * This adds the substitution l -> r to the auxiliary + * variable substitution subs_lhs -> subs_rhs, and serializes + * it (applies it to existing substitutions). + */ + void addToAuxVarSubstitution(std::vector<Node>& subs_lhs, + std::vector<Node>& subs_rhs, + Node l, + Node r); + /** cache bound variables for type returned + * by getBoundVariable(...). + */ + std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction> + d_bound_var; + /** current index of bound variables for type. + * The next call to getBoundVariable(...) for + * type tn returns the d_bound_var_index[tn]^th + * element of d_bound_var[tn], or a fresh variable + * if not in bounds. + */ + std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction> + d_bound_var_index; + //-------------------------------end cached per round + + //-------------------------------data per theory /** relevant theory ids * A list of theory ids that contain at least one * constraint in the body of the quantified formula we * are processing. */ std::vector<TheoryId> d_tids; + /** map from theory ids to instantiator preprocessors */ + std::map<TheoryId, InstantiatorPreprocess*> d_tipp; + /** registers all theory ids associated with type tn + * + * This recursively calls registerTheoryId for typeOf(tn') for + * all parameters and datatype subfields of type tn. + * visited stores the types we have already visited. + */ + void registerTheoryIds(TypeNode tn, std::map<TypeNode, bool>& visited); + /** register theory id tid + * + * This is called when the quantified formula we are processing + * with this class involves theory tid. In this case, we will + * construct instantiations based on the assertion list of this theory. + */ + void registerTheoryId(TheoryId tid); + //-------------------------------end data per theory + + //-------------------------------the variables + /** the variables we are instantiating + * For a quantified formula with n variables, + * the first n terms in d_vars are the instantiation + * constants corresponding to these variables. + */ + std::vector<Node> d_vars; + /** set form of d_vars */ + std::unordered_set<Node, NodeHashFunction> d_vars_set; + /** index of variables reported in instantiation */ + std::vector<unsigned> d_var_order_index; + /** number of input variables + * This is n for quantified formulas with n variables, + * and is at most the size of d_vars. + */ + unsigned d_num_input_variables; /** literals to equalities for aux vars * This stores entries of the form * L -> ( k -> t ) @@ -207,59 +391,64 @@ class CegInstantiator { * k=t1 and k=t2 respectively. */ std::map<Node, std::map<Node, Node> > d_aux_eq; - /** the variables we are instantiating - * These are the inst constants of the quantified formula - * we are processing. + /** auxiliary variables + * These variables include the result of removing ITE + * terms from the quantified formula we are processing. + * These variables must be eliminated from constraints + * as a preprocess step to check(). */ - std::vector<Node> d_vars; - /** set form of d_vars */ - std::unordered_set<Node, NodeHashFunction> d_vars_set; - /** index of variables reported in instantiation */ - std::vector<unsigned> d_var_order_index; - /** are we handled a nested quantified formula? */ + std::vector<Node> d_aux_vars; + /** register variable */ + void registerVariable(Node v, bool is_aux = false); + //-------------------------------the variables + + //-------------------------------quantified formula info + /** are we processing a nested quantified formula? */ bool d_is_nested_quant; /** the atoms of the CE lemma */ std::vector<Node> d_ce_atoms; - /** cache bound variables for type returned - * by getBoundVariable(...). - */ - std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction> - d_bound_var; - /** current index of bound variables for type. - * The next call to getBoundVariable(...) for - * type tn returns the d_bound_var_index[tn]^th - * element of d_bound_var[tn], or a fresh variable - * if not in bounds. - */ - std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction> - d_bound_var_index; /** collect atoms */ void collectCeAtoms(Node n, std::map<Node, bool>& visited); + //-------------------------------end quantified formula info - private: - //map from variables to their instantiators - std::map< Node, Instantiator * > d_instantiator; - //cache of current substitutions tried between register/unregister - std::map< Node, std::map< Node, std::map< Node, bool > > > d_curr_subs_proc; - std::map< Node, unsigned > d_curr_index; - //stack of temporary variables we are solving (e.g. subfields of datatypes) - std::vector< Node > d_stack_vars; + //-------------------------------current state + /** the current effort level of the instantiator + * This indicates the effort Instantiator objects + * will put into the terms they return. + */ + InstEffort d_effort; /** for each variable, the instantiator used for that variable */ - std::map< Node, Instantiator * > d_active_instantiators; - //register variable - void registerInstantiationVariable( Node v, unsigned index ); - void unregisterInstantiationVariable( Node v ); -private: - //for adding instantiations during check - void computeProgVars( Node n ); - // effort=0 : do not use model value, 1: use model value, 2: one must use model value - bool doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ); - // called by the above function after we finalize the variables/substitution and auxiliary lemmas - bool doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ); - //process - void processAssertions(); - void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); -private: + std::map<Node, Instantiator*> d_active_instantiators; + /** map from variables to the index in the prefix of the quantified + * formula we are processing. + */ + std::map<Node, unsigned> d_curr_index; + /** cache of current substitutions tried between activate/deactivate */ + std::map<Node, std::map<Node, std::map<Node, bool> > > d_curr_subs_proc; + /** stack of temporary variables we are solving for, + * e.g. subfields of datatypes. + */ + std::vector<Node> d_stack_vars; + /** activate instantiation variable v at index + * + * This is called when variable (inst constant) v is activated + * for the quantified formula we are processing. + * This method initializes the instantiator class for + * that variable if necessary, where this class is + * determined by the type of v. It also initializes + * the cache of values we have tried substituting for v + * (in d_curr_subs_proc), and stores its index. + */ + void activateInstantiationVariable(Node v, unsigned index); + /** deactivate instantiation variable + * + * This is called when variable (inst constant) v is deactivated + * for the quantified formula we are processing. + */ + void deactivateInstantiationVariable(Node v); + //-------------------------------end current state + + //---------------------------------for applying substitutions /** can use basic substitution */ bool canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ); /** apply substitution @@ -285,170 +474,268 @@ private: /** apply substitution to literal lit, with solved form expanded to subs/prop/non_basic/vars */ Node applySubstitutionToLiteral( Node lit, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, std::vector< Node >& non_basic ); + //---------------------------------end for applying substitutions + + /** map from variables to their instantiators */ + std::map<Node, Instantiator*> d_instantiator; + + /** construct instantiation + * This method constructs the current instantiation, where we + * are currently processing the i^th variable in d_vars. + * It returns true if a successful call to the output channel's + * doAddInstantiation was made. + */ + bool constructInstantiation(SolvedForm& sf, unsigned i); + /** do add instantiation + * This method is called by the above function after we finalize the + * variables/substitution and auxiliary lemmas. + * It returns true if a successful call to the output channel's + * doAddInstantiation was made. + */ + bool doAddInstantiation(std::vector<Node>& vars, + std::vector<Node>& subs, + std::vector<Node>& lemmas); +}; + +/** Instantiator class + * + * This is a virtual class that is used for methods for constructing + * substitutions for individual variables in counterexample-guided + * instantiation techniques. + * + * This class contains a set of interface functions below, which are called + * based on a fixed instantiation method implemented by CegInstantiator. + * In these calls, the Instantiator in turn makes calls to methods in + * CegInstanatior (primarily constructInstantiationInc). + */ +class Instantiator { public: - CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); - virtual ~CegInstantiator(); - //check : add instantiations based on valuation of d_vars - bool check(); - //presolve for quantified formula - void presolve( Node q ); - //register the counterexample lemma (stored in lems), modify vector - void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ); - //output - CegqiOutput * getOutput() { return d_out; } - //get quantifiers engine - QuantifiersEngine* getQuantifiersEngine() { return d_qe; } - //------------------------------interface for instantiators - /** push stack variable - * This adds a new variable to solve for in the stack - * of variables we are processing. This stack is only - * used for datatypes, where e.g. the DtInstantiator - * solving for a list x may push the stack "variables" - * head(x) and tail(x). + Instantiator( QuantifiersEngine * qe, TypeNode tn ); + virtual ~Instantiator(){} + /** reset + * This is called once, prior to any of the below methods are called. + * This function sets up any initial information necessary for constructing + * instantiations for pv based on the current context. */ - void pushStackVariable( Node v ); - /** pop stack variable */ - void popStackVariable(); - /** do add instantiation increment + virtual void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + } + + /** process equal term * - * Adds the substitution { pv_prop.getModifiedTerm(pv) -> n } to the current - * instantiation, specified by sf. + * This method is called when the entailment: + * E |= pv_prop.getModifiedTerm(pv) = n + * holds in the current context E, and n is eligible for instantiation. * - * This function returns true if a call to - * QuantifiersEngine::addInstantiation(...) - * was successfully made in a recursive call. - * - * The solved form sf is reverted to its original state if - * this function returns false, or - * revertOnSuccess is true and this function returns true. + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. */ - bool doAddInstantiationInc(Node pv, - Node n, - TermProperties& pv_prop, - SolvedForm& sf, - unsigned effort, - bool revertOnSuccess = false); - /** get the current model value of term n */ - Node getModelValue( Node n ); - /** get bound variable for type + virtual bool processEqualTerm(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + TermProperties& pv_prop, + Node n, + InstEffort effort); + /** process equal terms * - * This gets the next (canonical) bound variable of - * type tn. This can be used for instance when - * constructing instantiations that involve choice expressions. + * This method is called after process equal term, where eqc is the list of + * eligible terms in the equivalence class of pv. + * + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. */ - Node getBoundVariable(TypeNode tn); - //------------------------------end interface for instantiators - unsigned getNumCEAtoms() { return d_ce_atoms.size(); } - Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; } - /** is n a term that is eligible for instantiation? */ - bool isEligible( Node n ); - /** does n have variable pv? */ - bool hasVariable( Node n, Node pv ); - /** are we using delta for LRA virtual term substitution? */ - bool useVtsDelta() { return d_use_vts_delta; } - /** are we using infinity for LRA virtual term substitution? */ - bool useVtsInfinity() { return d_use_vts_inf; } - /** are we processing a nested quantified formula? */ - bool hasNestedQuantification() { return d_is_nested_quant; } -}; + virtual bool processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<Node>& eqc, + InstEffort effort) + { + return false; + } + /** whether the instantiator implements processEquality */ + virtual bool hasProcessEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + return false; + } + /** process equality + * The input is such that term_props.size() = terms.size() = 2 + * This method is called when the entailment: + * E ^ term_props[0].getModifiedTerm(x0) = + * terms[0] ^ term_props[1].getModifiedTerm(x1) = terms[1] |= x0 = x1 + * holds in current context E for fresh variables xi, terms[i] are eligible, + * and at least one terms[i] contains pv for i = 0,1. + * Notice in the basic case, E |= terms[0] = terms[1]. + * + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. + */ + virtual bool processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<TermProperties>& term_props, + std::vector<Node>& terms, + InstEffort effort) + { + return false; + } -// an instantiator for individual variables -// will make calls into CegInstantiator::doAddInstantiationInc -class Instantiator { -protected: - TypeNode d_type; - bool d_closed_enum_type; -public: - Instantiator( QuantifiersEngine * qe, TypeNode tn ); - virtual ~Instantiator(){} - virtual void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {} - - // Called when the entailment: - // E |= pv_prop.getModifiedTerm(pv) = n - // holds in the current context E, and n is eligible for instantiation. - virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ); - // Called about process equal term, where eqc is the list of eligible terms in the equivalence class of pv - virtual bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { return false; } - - // whether the instantiator implements processEquality - virtual bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } - // term_props.size() = terms.size() = 2 - // Called when the entailment: - // E ^ term_props[0].getModifiedTerm(x0) = terms[0] ^ term_props[1].getModifiedTerm(x1) = terms[1] |= x0 = x1 - // holds in current context E for fresh variables xi, terms[i] are eligible, and at least one terms[i] contains pv for i = 0,1. - // Notice in the basic case, E |= terms[0] = terms[1]. - // Returns true if an instantiation was successfully added via a recursive call - virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { return false; } - - // whether the instantiator implements processAssertion for any literal - virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } + /** whether the instantiator implements processAssertion for any literal */ + virtual bool hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + return false; + } /** has process assertion * - * Called when the entailment: + * This method is called when the entailment: * E |= lit * holds in current context E. Typically, lit belongs to the list of current * assertions. * - * This function is used to determine whether the instantiator implements + * This method is used to determine whether the instantiator implements * processAssertion for literal lit. - * If this function returns null, then this intantiator does not handle the - * literal lit - * Otherwise, this function returns a literal lit' with the properties: + * If this method returns null, then this intantiator does not handle the + * literal lit. Otherwise, this method returns a literal lit' such that: * (1) lit' is true in the current model, * (2) lit' implies lit. * where typically lit' = lit. */ - virtual Node hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, - Node lit, unsigned effort) { + virtual Node hasProcessAssertion( + CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, InstEffort effort) + { return Node::null(); } /** process assertion - * Processes the assertion slit for variable pv - * - * lit is the substituted form (under sf) of a literal returned by - * hasProcessAssertion - * alit is the asserted literal, given as input to hasProcessAssertion - * - * Returns true if an instantiation was successfully added via a recursive call - */ - virtual bool processAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, - Node lit, Node alit, unsigned effort) { + * This method processes the assertion slit for variable pv. + * lit : the substituted form (under sf) of a literal returned by + * hasProcessAssertion + * alit : the asserted literal, given as input to hasProcessAssertion + * + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. + */ + virtual bool processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + InstEffort effort) + { return false; } /** process assertions - * Called after processAssertion is called for each literal asserted to the - * instantiator. - */ - virtual bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv, - unsigned effort) { + * + * Called after processAssertion is called for each literal asserted to the + * instantiator. + * + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. + */ + virtual bool processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { return false; } - //do we use the model value as instantiation for pv - virtual bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } - //do we allow the model value as instantiation for pv - virtual bool allowModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return d_closed_enum_type; } + /** do we use the model value as instantiation for pv? + * This method returns true if we use model value instantiations + * at the same effort level as those determined by this instantiator. + */ + virtual bool useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + return false; + } + /** do we allow the model value as instantiation for pv? */ + virtual bool allowModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + return d_closed_enum_type; + } - //do we need to postprocess the solved form for pv? - virtual bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } - //postprocess the solved form for pv, returns true if we successfully postprocessed, lemmas is a set of lemmas we wish to return along with the instantiation - virtual bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas ) { return true; } + /** do we need to postprocess the solved form for pv? */ + virtual bool needsPostProcessInstantiationForVariable(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + return false; + } + /** postprocess the solved form for pv + * + * This method returns true if we successfully postprocessed the solved form. + * lemmas is a set of lemmas we wish to return along with the instantiation. + */ + virtual bool postProcessInstantiationForVariable(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort, + std::vector<Node>& lemmas) + { + return true; + } /** Identify this module (for debugging) */ virtual std::string identify() const { return "Default"; } + protected: + /** the type of the variable we are instantiating */ + TypeNode d_type; + /** whether d_type is a closed enumerable type */ + bool d_closed_enum_type; }; class ModelValueInstantiator : public Instantiator { public: ModelValueInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} virtual ~ModelValueInstantiator(){} - bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } + bool useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + InstEffort effort) + { + return true; + } std::string identify() const { return "ModelValue"; } }; -} -} -} +/** instantiator preprocess + * + * This class implements techniques for preprocessing the counterexample lemma + * generated for counterexample-guided quantifier instantiation. + */ +class InstantiatorPreprocess +{ + public: + InstantiatorPreprocess() {} + virtual ~InstantiatorPreprocess() {} + /** register counterexample lemma + * This implements theory-specific preprocessing and registration + * of counterexample lemmas, with the same contract as + * CegInstantiation::registerCounterexampleLemma. + */ + virtual void registerCounterexampleLemma(std::vector<Node>& lems, + std::vector<Node>& ce_vars) + { + } +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ #endif |