/** get term database sygus */
quantifiers::TermDbSygus* getTermDatabaseSygus() const;
//---------------------- end utilities
- private:
- //---------------------- private initialization
- /**
- * Finish initialize, which passes pointers to the objects that quantifiers
- * engine needs but were not available when it was created. This is
- * called after theories have been created but before they have finished
- * initialization.
- *
- * @param te The theory engine
- * @param dm The decision manager of the theory engine
- */
- void finishInit(TheoryEngine* te);
- //---------------------- end private initialization
-
- public:
/** presolve */
void presolve();
/** notify preprocessed assertion */
void preRegisterQuantifier(Node q);
/** assert universal quantifier */
void assertQuantifier( Node q, bool pol );
-private:
- /** (context-indepentent) register quantifier internal
- *
- * This is called when a quantified formula q is pre-registered to the
- * quantifiers theory, and updates the modules in this class with
- * context-independent information about how to handle q. This includes basic
- * information such as which module owns q.
- */
- void registerQuantifierInternal(Node q);
- /** reduceQuantifier, return true if reduced */
- bool reduceQuantifier(Node q);
-
-public:
- /** notification when master equality engine is updated */
- void eqNotifyNewClass(TNode t);
- /** mark relevant quantified formula, this will indicate it should be checked
- * before the others */
- void markRelevant(Node q);
- /**
- * Get quantifiers name, which returns a variable corresponding to the name of
- * quantified formula q if q has a name, or otherwise returns q itself.
- */
- Node getNameForQuant(Node q) const;
- /**
- * Get name for quantified formula. Returns true if q has a name or if req
- * is false. Sets name to the result of the above method.
- */
- bool getNameForQuant(Node q, Node& name, bool req = true) const;
-
-public:
- //----------user interface for instantiations (see quantifiers/instantiate.h)
- /** get list of quantified formulas that were instantiated */
- void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
- /** get instantiation term vectors */
- void getInstantiationTermVectors(Node q,
- std::vector<std::vector<Node> >& tvecs);
- void getInstantiationTermVectors(
- std::map<Node, std::vector<std::vector<Node> > >& insts);
- /**
- * Get instantiations for quantified formula q. If q is (forall ((x T)) (P x)),
- * this is a list of the form (P t1) ... (P tn) for ground terms ti.
- */
- void getInstantiations(Node q, std::vector<Node>& insts);
- /**
- * Get skolemization vectors, where for each quantified formula that was
- * skolemized, this is the list of skolems that were used to witness the
- * negation of that quantified formula.
- */
- void getSkolemTermVectors(std::map<Node, std::vector<Node> >& sks) const;
-
- /** get synth solutions
- *
- * This method returns true if there is a synthesis solution available. This
- * is the case if the last call to check satisfiability originated in a
- * check-synth call, and the synthesis engine module of this class
- * successfully found a solution for all active synthesis conjectures.
- *
- * This method adds entries to sol_map that map functions-to-synthesize with
- * their solutions, for all active conjectures. This should be called
- * immediately after the solver answers unsat for sygus input.
- *
- * For details on what is added to sol_map, see
- * SynthConjecture::getSynthSolutions.
- */
- bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
- /** Declare pool */
- void declarePool(Node p, const std::vector<Node>& initValue);
- //----------end user interface for instantiations
+ /** notification when master equality engine is updated */
+ void eqNotifyNewClass(TNode t);
+ /** mark relevant quantified formula, this will indicate it should be checked
+ * before the others */
+ void markRelevant(Node q);
+ /**
+ * Get quantifiers name, which returns a variable corresponding to the name of
+ * quantified formula q if q has a name, or otherwise returns q itself.
+ */
+ Node getNameForQuant(Node q) const;
+ /**
+ * Get name for quantified formula. Returns true if q has a name or if req
+ * is false. Sets name to the result of the above method.
+ */
+ bool getNameForQuant(Node q, Node& name, bool req = true) const;
+ //----------user interface for instantiations (see quantifiers/instantiate.h)
+ /** get list of quantified formulas that were instantiated */
+ void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
+ /** get instantiation term vectors */
+ void getInstantiationTermVectors(Node q,
+ std::vector<std::vector<Node> >& tvecs);
+ void getInstantiationTermVectors(
+ std::map<Node, std::vector<std::vector<Node> > >& insts);
+ /**
+ * Get instantiations for quantified formula q. If q is (forall ((x T)) (P
+ * x)), this is a list of the form (P t1) ... (P tn) for ground terms ti.
+ */
+ void getInstantiations(Node q, std::vector<Node>& insts);
+ /**
+ * Get skolemization vectors, where for each quantified formula that was
+ * skolemized, this is the list of skolems that were used to witness the
+ * negation of that quantified formula.
+ */
+ void getSkolemTermVectors(std::map<Node, std::vector<Node> >& sks) const;
+ /** get synth solutions
+ *
+ * This method returns true if there is a synthesis solution available. This
+ * is the case if the last call to check satisfiability originated in a
+ * check-synth call, and the synthesis engine module of this class
+ * successfully found a solution for all active synthesis conjectures.
+ *
+ * This method adds entries to sol_map that map functions-to-synthesize with
+ * their solutions, for all active conjectures. This should be called
+ * immediately after the solver answers unsat for sygus input.
+ *
+ * For details on what is added to sol_map, see
+ * SynthConjecture::getSynthSolutions.
+ */
+ bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
+ /** Declare pool */
+ void declarePool(Node p, const std::vector<Node>& initValue);
+ //----------end user interface for instantiations
private:
+ //---------------------- private initialization
+ /**
+ * Finish initialize, which passes pointers to the objects that quantifiers
+ * engine needs but were not available when it was created. This is
+ * called after theories have been created but before they have finished
+ * initialization.
+ *
+ * @param te The theory engine
+ * @param dm The decision manager of the theory engine
+ */
+ void finishInit(TheoryEngine* te);
+ //---------------------- end private initialization
+ /** (context-indepentent) register quantifier internal
+ *
+ * This is called when a quantified formula q is pre-registered to the
+ * quantifiers theory, and updates the modules in this class with
+ * context-independent information about how to handle q. This includes basic
+ * information such as which module owns q.
+ */
+ void registerQuantifierInternal(Node q);
+ /** reduceQuantifier, return true if reduced */
+ bool reduceQuantifier(Node q);
+
/** The quantifiers state object */
quantifiers::QuantifiersState& d_qstate;
/** The quantifiers inference manager */
projects / cvc5.git / commitdiff