/**
* Does non-context dependent setup for a node connected to a theory.
*/
- void preRegisterTerm(TNode n);
+ void preRegisterTerm(TNode n) override;
- Node expandDefinition(LogicRequest &logicRequest, Node node);
+ Node expandDefinition(LogicRequest& logicRequest, Node node) override;
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
- void check(Effort e);
- bool needsCheckLastEffort();
- void propagate(Effort e);
- Node explain(TNode n);
- bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
- bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp );
+ void check(Effort e) override;
+ bool needsCheckLastEffort() override;
+ void propagate(Effort e) override;
+ Node explain(TNode n) override;
+ bool getCurrentSubstitution(int effort,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs,
+ std::map<Node, std::vector<Node> >& exp) override;
+ bool isExtfReduced(int effort,
+ Node n,
+ Node on,
+ std::vector<Node>& exp) override;
bool collectModelInfo(TheoryModel* m) override;
- void shutdown(){ }
+ void shutdown() override {}
- void presolve();
- void notifyRestart();
- PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
- Node ppRewrite(TNode atom);
- void ppStaticLearn(TNode in, NodeBuilder<>& learned);
+ void presolve() override;
+ void notifyRestart() override;
+ PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
+ Node ppRewrite(TNode atom) override;
+ void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
- std::string identify() const { return std::string("TheoryArith"); }
+ std::string identify() const override { return std::string("TheoryArith"); }
- EqualityStatus getEqualityStatus(TNode a, TNode b);
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
- void addSharedTerm(TNode n);
+ void addSharedTerm(TNode n) override;
- Node getModelValue(TNode var);
+ Node getModelValue(TNode var) override;
-
- std::pair<bool, Node> entailmentCheck(TNode lit,
- const EntailmentCheckParameters* params,
- EntailmentCheckSideEffects* out);
+ std::pair<bool, Node> entailmentCheck(
+ TNode lit,
+ const EntailmentCheckParameters* params,
+ EntailmentCheckSideEffects* out) override;
};/* class TheoryArith */
std::string name = "");
~TheoryArrays();
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
- std::string identify() const { return std::string("TheoryArrays"); }
+ std::string identify() const override { return std::string("TheoryArrays"); }
/////////////////////////////////////////////////////////////////////////////
// PREPROCESSING
bool ppDisequal(TNode a, TNode b);
Node solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck);
- public:
-
- PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
- Node ppRewrite(TNode atom);
+ public:
+ PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
+ Node ppRewrite(TNode atom) override;
/////////////////////////////////////////////////////////////////////////////
// T-PROPAGATION / REGISTRATION
/////////////////////////////////////////////////////////////////////////////
- private:
-
+ private:
/** Literals to propagate */
context::CDList<Node> d_literalsToPropagate;
/** Helper for preRegisterTerm, also used internally */
void preRegisterTermInternal(TNode n);
- public:
-
- void preRegisterTerm(TNode n);
- void propagate(Effort e);
+ public:
+ void preRegisterTerm(TNode n) override;
+ void propagate(Effort e) override;
Node explain(TNode n, eq::EqProof* proof);
- Node explain(TNode n);
+ Node explain(TNode n) override;
/////////////////////////////////////////////////////////////////////////////
// SHARING
/////////////////////////////////////////////////////////////////////////////
- private:
-
+ private:
class MayEqualNotifyClass {
public:
bool notify(TNode propagation) { return true; }
// Helper for computeCareGraph
void checkPair(TNode r1, TNode r2);
- public:
-
- void addSharedTerm(TNode t);
- EqualityStatus getEqualityStatus(TNode a, TNode b);
- void computeCareGraph();
+ public:
+ void addSharedTerm(TNode t) override;
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+ void computeCareGraph() override;
bool isShared(TNode t)
- { return (d_sharedArrays.find(t) != d_sharedArrays.end()); }
-
+ {
+ return (d_sharedArrays.find(t) != d_sharedArrays.end());
+ }
/////////////////////////////////////////////////////////////////////////////
// MODEL GENERATION
/////////////////////////////////////////////////////////////////////////////
- private:
-
- public:
- bool collectModelInfo(TheoryModel* m) override;
-
- /////////////////////////////////////////////////////////////////////////////
- // NOTIFICATIONS
- /////////////////////////////////////////////////////////////////////////////
+ public:
+ bool collectModelInfo(TheoryModel* m) override;
- private:
- public:
+ /////////////////////////////////////////////////////////////////////////////
+ // NOTIFICATIONS
+ /////////////////////////////////////////////////////////////////////////////
- Node getNextDecisionRequest( unsigned& priority );
+ public:
+ Node getNextDecisionRequest(unsigned& priority) override;
- void presolve();
- void shutdown() { }
+ void presolve() override;
+ void shutdown() override {}
/////////////////////////////////////////////////////////////////////////////
// MAIN SOLVER
/////////////////////////////////////////////////////////////////////////////
- public:
-
- void check(Effort e);
-
- private:
+ public:
+ void check(Effort e) override;
+ private:
TNode weakEquivGetRep(TNode node);
TNode weakEquivGetRepIndex(TNode node, TNode index);
void visitAllLeaves(TNode reason, std::vector<TNode>& conjunctions);
/** An equality-engine callback for proof reconstruction */
ArrayProofReconstruction d_proofReconstruction;
- public:
-
- eq::EqualityEngine* getEqualityEngine() {
- return &d_equalityEngine;
- }
+ public:
+ eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
};/* class TheoryArrays */
~TheoryBV();
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
- Node expandDefinition(LogicRequest &logicRequest, Node node);
+ Node expandDefinition(LogicRequest& logicRequest, Node node) override;
void mkAckermanizationAssertions(std::vector<Node>& assertions);
- void preRegisterTerm(TNode n);
+ void preRegisterTerm(TNode n) override;
- void check(Effort e);
-
- bool needsCheckLastEffort();
+ void check(Effort e) override;
+
+ bool needsCheckLastEffort() override;
- void propagate(Effort e);
+ void propagate(Effort e) override;
- Node explain(TNode n);
+ Node explain(TNode n) override;
bool collectModelInfo(TheoryModel* m) override;
- std::string identify() const { return std::string("TheoryBV"); }
+ std::string identify() const override { return std::string("TheoryBV"); }
/** equality engine */
- eq::EqualityEngine * getEqualityEngine();
- bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
- int getReduction( int effort, Node n, Node& nr );
-
- PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+ eq::EqualityEngine* getEqualityEngine() override;
+ bool getCurrentSubstitution(int effort,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs,
+ std::map<Node, std::vector<Node> >& exp) override;
+ int getReduction(int effort, Node n, Node& nr) override;
+
+ PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
void enableCoreTheorySlicer();
- Node ppRewrite(TNode t);
+ Node ppRewrite(TNode t) override;
- void ppStaticLearn(TNode in, NodeBuilder<>& learned);
+ void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
- void presolve();
+ void presolve() override;
bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
*/
void explain(TNode literal, std::vector<TNode>& assumptions);
- void addSharedTerm(TNode t);
+ void addSharedTerm(TNode t) override;
bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
- EqualityStatus getEqualityStatus(TNode a, TNode b);
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
- Node getModelValue(TNode var);
+ Node getModelValue(TNode var) override;
inline std::string indent()
{
/** get eqc constructor */
TNode getEqcConstructor( TNode r );
-protected:
+ protected:
void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs );
/** compute care graph */
- void computeCareGraph();
+ void computeCareGraph() override;
-public:
+ public:
TheoryDatatypes(context::Context* c, context::UserContext* u,
OutputChannel& out, Valuation valuation,
const LogicInfo& logicInfo);
~TheoryDatatypes();
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
/** propagate */
- void propagate(Effort effort);
+ void propagate(Effort effort) override;
/** propagate */
bool propagate(TNode literal);
/** explain */
void explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions );
void explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions );
void explain( TNode literal, std::vector<TNode>& assumptions );
- Node explain( TNode literal );
+ Node explain(TNode literal) override;
Node explain( std::vector< Node >& lits );
/** Conflict when merging two constants */
void conflict(TNode a, TNode b);
/** called when two equivalence classes are made disequal */
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
- void check(Effort e);
- bool needsCheckLastEffort();
- void preRegisterTerm(TNode n);
- void finishInit();
- Node expandDefinition(LogicRequest &logicRequest, Node n);
- Node ppRewrite(TNode n);
- void presolve();
- void addSharedTerm(TNode t);
- EqualityStatus getEqualityStatus(TNode a, TNode b);
+ void check(Effort e) override;
+ bool needsCheckLastEffort() override;
+ void preRegisterTerm(TNode n) override;
+ void finishInit() override;
+ Node expandDefinition(LogicRequest& logicRequest, Node n) override;
+ Node ppRewrite(TNode n) override;
+ void presolve() override;
+ void addSharedTerm(TNode t) override;
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
bool collectModelInfo(TheoryModel* m) override;
- void shutdown() { }
- std::string identify() const { return std::string("TheoryDatatypes"); }
+ void shutdown() override {}
+ std::string identify() const override
+ {
+ return std::string("TheoryDatatypes");
+ }
/** equality engine */
- eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; }
- bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
+ eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
+ bool getCurrentSubstitution(int effort,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs,
+ std::map<Node, std::vector<Node> >& exp) override;
/** debug print */
void printModelDebug( const char* c );
/** entailment check */
- virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL);
-private:
+ std::pair<bool, Node> entailmentCheck(
+ TNode lit,
+ const EntailmentCheckParameters* params = NULL,
+ EntailmentCheckSideEffects* out = NULL) override;
+
+ private:
/** add tester to equivalence class info */
void addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg );
/** add selector to equivalence class info */
SygusSymBreakNew* d_sygus_sym_break;
public:
- Node getNextDecisionRequest( unsigned& priority );
+ Node getNextDecisionRequest(unsigned& priority) override;
};/* class TheoryDatatypes */
}/* CVC4::theory::datatypes namespace */
TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out,
Valuation valuation, const LogicInfo& logicInfo);
- Node expandDefinition(LogicRequest& lr, Node node);
+ Node expandDefinition(LogicRequest& lr, Node node) override;
- void preRegisterTerm(TNode node);
- void addSharedTerm(TNode node);
+ void preRegisterTerm(TNode node) override;
+ void addSharedTerm(TNode node) override;
- void check(Effort);
+ void check(Effort) override;
- Node getModelValue(TNode var);
+ Node getModelValue(TNode var) override;
bool collectModelInfo(TheoryModel* m) override;
- std::string identify() const { return "THEORY_FP"; }
+ std::string identify() const override { return "THEORY_FP"; }
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
- Node explain(TNode n);
+ Node explain(TNode n) override;
protected:
/** Equality engine */
class BvInstantiator : public Instantiator {
public:
BvInstantiator(QuantifiersEngine* qe, TypeNode tn);
- virtual ~BvInstantiator();
- virtual void reset(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort) override;
- virtual bool hasProcessAssertion(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort) override
+ ~BvInstantiator() override;
+ void reset(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override;
+ bool hasProcessAssertion(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override
{
return true;
}
- virtual Node hasProcessAssertion(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- Node lit,
- CegInstEffort effort) override;
- virtual bool processAssertion(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- Node lit,
- Node alit,
- CegInstEffort effort) override;
- virtual bool processAssertions(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort) override;
+ Node hasProcessAssertion(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ Node lit,
+ CegInstEffort effort) override;
+ bool processAssertion(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ Node lit,
+ Node alit,
+ CegInstEffort effort) override;
+ bool processAssertions(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override;
/** use model value
*
* We allow model values if we have not already tried an assertion,
* and only at levels below full if cbqiFullEffort is false.
*/
- virtual bool useModelValue(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort) override;
- virtual std::string identify() const { return "Bv"; }
+ bool useModelValue(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override;
+ std::string identify() const override { return "Bv"; }
+
private:
// point to the bv inverter class
BvInverter * d_inverter;
{
public:
BvInstantiatorPreprocess() {}
- virtual ~BvInstantiatorPreprocess() {}
+ ~BvInstantiatorPreprocess() override {}
/** register counterexample lemma
*
* This method modifies the contents of lems based on the extract terms
* since the added equalities ensure we are able to construct the proper
* solved forms for variables in t and for the intermediate variables above.
*/
- virtual void registerCounterexampleLemma(std::vector<Node>& lems,
- std::vector<Node>& ce_vars) override;
+ void registerCounterexampleLemma(std::vector<Node>& lems,
+ std::vector<Node>& ce_vars) override;
private:
/** collect extracts
class FirstOrderModelFmc : public FirstOrderModel
{
friend class FullModelChecker;
-private:
+
+ private:
/** models for UF */
std::map<Node, Def * > d_models;
std::map<TypeNode, Node > d_type_star;
Node intervalOp;
/** get current model value */
- void processInitializeModelForTerm(Node n);
-public:
+ void processInitializeModelForTerm(Node n) override;
+
+ public:
FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
~FirstOrderModelFmc() override;
- FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
+ FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; }
// initialize the model
- void processInitialize( bool ispre );
+ void processInitialize(bool ispre) override;
Node getFunctionValue(Node op, const char* argPrefix );
bool isStar(Node n);
*
* See Trigger::getActiveScore for details.
*/
- int getActiveScore(QuantifiersEngine* qe);
+ int getActiveScore(QuantifiersEngine* qe) override;
/** exclude match
*
* Exclude matching d_match_pattern with Node n on subsequent calls to
};
class InstStrategyCegqi : public InstStrategyCbqi {
-protected:
+ protected:
CegqiOutputInstStrategy * d_out;
std::map< Node, CegInstantiator * > d_cinst;
Node d_small_const;
Node d_curr_quant;
bool d_check_vts_lemma_lc;
/** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
- void process( Node f, Theory::Effort effort, int e );
+ void processResetInstantiationRound(Theory::Effort effort) override;
+ void process(Node f, Theory::Effort effort, int e) override;
/** register ce lemma */
- void registerCounterexampleLemma( Node q, Node lem );
-public:
+ void registerCounterexampleLemma(Node q, Node lem) override;
+
+ public:
InstStrategyCegqi( QuantifiersEngine * qe );
~InstStrategyCegqi() override;
bool isEligibleForInstantiation( Node n );
bool addLemma( Node lem );
/** identify */
- std::string identify() const { return std::string("Cegqi"); }
+ std::string identify() const override { return std::string("Cegqi"); }
//get instantiator for quantifier
CegInstantiator * getInstantiator( Node q );
//register quantifier
- void registerQuantifier( Node q );
+ void registerQuantifier(Node q) override;
//presolve
- void presolve();
+ void presolve() override;
};
}
//do InstGen techniques for quantifier, return number of lemmas produced
int doInstGen(FirstOrderModel* fm, Node f) override;
//theory-specific build models
- void constructModelUf( FirstOrderModel* fm, Node op );
+ void constructModelUf(FirstOrderModel* fm, Node op) override;
protected:
std::map< Node, QuantPhaseReq > d_phase_reqs;
//options
bool optReconsiderFuncConstants() { return true; }
//has inst gen
- bool hasInstGen( Node f ) { return !d_quant_selection_lit[f].isNull(); }
+ bool hasInstGen(Node f) override
+ {
+ return !d_quant_selection_lit[f].isNull();
+ }
};
}/* CVC4::theory::quantifiers namespace */
namespace quantifiers {
class TheoryQuantifiers : public Theory {
-private:
- typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
- /** number of instantiations */
- int d_numInstantiations;
- int d_baseDecLevel;
-private:
- void computeCareGraph();
-
-public:
+ public:
TheoryQuantifiers(context::Context* c, context::UserContext* u,
OutputChannel& out, Valuation valuation,
const LogicInfo& logicInfo);
~TheoryQuantifiers();
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
- void addSharedTerm(TNode t);
+ void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+ void addSharedTerm(TNode t) override;
void notifyEq(TNode lhs, TNode rhs);
- void preRegisterTerm(TNode n);
- void presolve();
- void ppNotifyAssertions(const std::vector<Node>& assertions);
- void check(Effort e);
- Node getNextDecisionRequest( unsigned& priority );
+ void preRegisterTerm(TNode n) override;
+ void presolve() override;
+ void ppNotifyAssertions(const std::vector<Node>& assertions) override;
+ void check(Effort e) override;
+ Node getNextDecisionRequest(unsigned& priority) override;
Node getValue(TNode n);
bool collectModelInfo(TheoryModel* m) override;
- void shutdown() { }
- std::string identify() const { return std::string("TheoryQuantifiers"); }
- void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value);
- bool ppDontRewriteSubterm(TNode atom) { return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; }
-private:
+ void shutdown() override {}
+ std::string identify() const override
+ {
+ return std::string("TheoryQuantifiers");
+ }
+ void setUserAttribute(const std::string& attr,
+ Node n,
+ std::vector<Node> node_values,
+ std::string str_value) override;
+ bool ppDontRewriteSubterm(TNode atom) override
+ {
+ return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS;
+ }
+
+ private:
void assertUniversal( Node n );
void assertExistential( Node n );
+ void computeCareGraph() override;
+
+ using BoolMap = context::CDHashMap<Node, bool, NodeHashFunction>;
+
+ /** number of instantiations */
+ int d_numInstantiations;
+ int d_baseDecLevel;
+
};/* class TheoryQuantifiers */
}/* CVC4::theory::quantifiers namespace */
// MISC
/////////////////////////////////////////////////////////////////////////////
- private:
+ private:
/** all lemmas sent */
NodeSet d_lemmas_produced_c;
std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict,
bool pol, bool hasPol, bool underSpatial );
- public:
-
+ public:
TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
~TheorySep();
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
- std::string identify() const { return std::string("TheorySep"); }
+ std::string identify() const override { return std::string("TheorySep"); }
/////////////////////////////////////////////////////////////////////////////
// PREPROCESSING
/////////////////////////////////////////////////////////////////////////////
- public:
-
- PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
- Node ppRewrite(TNode atom);
+ public:
+ PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
+ Node ppRewrite(TNode atom) override;
- void ppNotifyAssertions(const std::vector<Node>& assertions);
+ void ppNotifyAssertions(const std::vector<Node>& assertions) override;
/////////////////////////////////////////////////////////////////////////////
// T-PROPAGATION / REGISTRATION
/////////////////////////////////////////////////////////////////////////////
- private:
-
+ private:
/** Should be called to propagate the literal. */
bool propagate(TNode literal);
/** Explain why this literal is true by adding assumptions */
void explain(TNode literal, std::vector<TNode>& assumptions);
- public:
+ public:
+ void propagate(Effort e) override;
+ Node explain(TNode n) override;
- void propagate(Effort e);
- Node explain(TNode n);
-
- public:
-
- void addSharedTerm(TNode t);
- EqualityStatus getEqualityStatus(TNode a, TNode b);
- void computeCareGraph();
+ public:
+ void addSharedTerm(TNode t) override;
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+ void computeCareGraph() override;
/////////////////////////////////////////////////////////////////////////////
// MODEL GENERATION
/////////////////////////////////////////////////////////////////////////////
- public:
- bool collectModelInfo(TheoryModel* m) override;
- void postProcessModel(TheoryModel* m);
-
- /////////////////////////////////////////////////////////////////////////////
- // NOTIFICATIONS
- /////////////////////////////////////////////////////////////////////////////
+ public:
+ bool collectModelInfo(TheoryModel* m) override;
+ void postProcessModel(TheoryModel* m) override;
- private:
- public:
+ /////////////////////////////////////////////////////////////////////////////
+ // NOTIFICATIONS
+ /////////////////////////////////////////////////////////////////////////////
- Node getNextDecisionRequest( unsigned& priority );
+ public:
+ Node getNextDecisionRequest(unsigned& priority) override;
- void presolve();
- void shutdown() { }
+ void presolve() override;
+ void shutdown() override {}
/////////////////////////////////////////////////////////////////////////////
// MAIN SOLVER
/////////////////////////////////////////////////////////////////////////////
- public:
-
- void check(Effort e);
+ public:
+ void check(Effort e) override;
- bool needsCheckLastEffort();
+ bool needsCheckLastEffort() override;
- private:
-
- // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
- class NotifyClass : public eq::EqualityEngineNotify {
+ private:
+ // NotifyClass: template helper class for d_equalityEngine - handles
+ // call-back from congruence closure module
+ class NotifyClass : public eq::EqualityEngineNotify
+ {
TheorySep& d_sep;
- public:
- NotifyClass(TheorySep& sep): d_sep(sep) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) {
- Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
+ public:
+ NotifyClass(TheorySep& sep) : d_sep(sep) {}
+
+ bool eqNotifyTriggerEquality(TNode equality, bool value)
+ {
+ Debug("sep::propagate")
+ << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", "
+ << (value ? "true" : "false") << ")" << std::endl;
// Just forward to sep
- if (value) {
+ if (value)
+ {
return d_sep.propagate(equality);
- } else {
+ }
+ else
+ {
return d_sep.propagate(equality.notNode());
}
}
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value)
+ {
Unreachable();
}
- bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
- Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
- if (value) {
+ bool eqNotifyTriggerTermEquality(TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value)
+ {
+ Debug("sep::propagate")
+ << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2
+ << ", " << (value ? "true" : "false") << ")" << std::endl;
+ if (value)
+ {
// Propagate equality between shared terms
return d_sep.propagate(t1.eqNode(t2));
- } else {
+ }
+ else
+ {
return d_sep.propagate(t1.eqNode(t2).notNode());
}
return true;
}
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
- Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2)
+ {
+ Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1
+ << ", " << t2 << ")" << std::endl;
d_sep.conflict(t1, t2);
}
- void eqNotifyNewClass(TNode t) { }
- void eqNotifyPreMerge(TNode t1, TNode t2) { d_sep.eqNotifyPreMerge( t1, t2 ); }
- void eqNotifyPostMerge(TNode t1, TNode t2) { d_sep.eqNotifyPostMerge( t1, t2 ); }
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+ void eqNotifyNewClass(TNode t) {}
+ void eqNotifyPreMerge(TNode t1, TNode t2)
+ {
+ d_sep.eqNotifyPreMerge(t1, t2);
+ }
+ void eqNotifyPostMerge(TNode t1, TNode t2)
+ {
+ d_sep.eqNotifyPostMerge(t1, t2);
+ }
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {}
};
/** The notify class for d_equalityEngine */
void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active );
Node mkUnion( TypeNode tn, std::vector< Node >& locs );
-private:
+
+ private:
Node getRepresentative( Node t );
bool hasTerm( Node a );
bool areEqual( Node a, Node b );
void sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer = false );
void doPendingFacts();
-public:
- eq::EqualityEngine* getEqualityEngine() {
- return &d_equalityEngine;
- }
+
+ public:
+ eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
void initializeBounds();
};/* class TheorySep */
~TheorySets();
- void addSharedTerm(TNode);
+ void addSharedTerm(TNode) override;
- void check(Effort);
-
- bool needsCheckLastEffort();
+ void check(Effort) override;
+
+ bool needsCheckLastEffort() override;
bool collectModelInfo(TheoryModel* m) override;
- void computeCareGraph();
+ void computeCareGraph() override;
+
+ Node explain(TNode) override;
- Node explain(TNode);
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
- EqualityStatus getEqualityStatus(TNode a, TNode b);
+ Node getModelValue(TNode) override;
- Node getModelValue(TNode);
+ std::string identify() const override { return "THEORY_SETS"; }
- std::string identify() const { return "THEORY_SETS"; }
+ void preRegisterTerm(TNode node) override;
- void preRegisterTerm(TNode node);
+ Node expandDefinition(LogicRequest& logicRequest, Node n) override;
- Node expandDefinition(LogicRequest &logicRequest, Node n);
+ PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
- PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+ void presolve() override;
- void presolve();
+ void propagate(Effort) override;
- void propagate(Effort);
+ void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
-
bool isEntailed( Node n, bool pol );
};/* class TheorySets */
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-public:
+ public:
TheoryStrings(context::Context* c, context::UserContext* u,
OutputChannel& out, Valuation valuation,
const LogicInfo& logicInfo);
~TheoryStrings();
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
- std::string identify() const { return std::string("TheoryStrings"); }
+ std::string identify() const override { return std::string("TheoryStrings"); }
-public:
- void propagate(Effort e);
+ public:
+ void propagate(Effort e) override;
bool propagate(TNode literal);
void explain( TNode literal, std::vector<TNode>& assumptions );
- Node explain( TNode literal );
- eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; }
- bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
- int getReduction( int effort, Node n, Node& nr );
-
+ Node explain(TNode literal) override;
+ eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
+ bool getCurrentSubstitution(int effort,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs,
+ std::map<Node, std::vector<Node> >& exp) override;
+ int getReduction(int effort, Node n, Node& nr) override;
+
// NotifyClass for equality engine
class NotifyClass : public eq::EqualityEngineNotify {
TheoryStrings& d_str;
/////////////////////////////////////////////////////////////////////////////
// MODEL GENERATION
/////////////////////////////////////////////////////////////////////////////
-public:
- bool collectModelInfo(TheoryModel* m) override;
+ public:
+ bool collectModelInfo(TheoryModel* m) override;
- /////////////////////////////////////////////////////////////////////////////
- // NOTIFICATIONS
- /////////////////////////////////////////////////////////////////////////////
-public:
- void presolve();
- void shutdown() { }
+ /////////////////////////////////////////////////////////////////////////////
+ // NOTIFICATIONS
+ /////////////////////////////////////////////////////////////////////////////
+ public:
+ void presolve() override;
+ void shutdown() override {}
/////////////////////////////////////////////////////////////////////////////
// MAIN SOLVER
/////////////////////////////////////////////////////////////////////////////
-private:
- void addSharedTerm(TNode n);
- EqualityStatus getEqualityStatus(TNode a, TNode b);
+ private:
+ void addSharedTerm(TNode n) override;
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
-private:
+ private:
class EqcInfo {
public:
EqcInfo( context::Context* c );
//cardinality check
void checkCardinality();
-private:
+ private:
void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
-public:
+
+ public:
/** preregister term */
- void preRegisterTerm(TNode n);
+ void preRegisterTerm(TNode n) override;
/** Expand definition */
- Node expandDefinition(LogicRequest &logicRequest, Node n);
+ Node expandDefinition(LogicRequest& logicRequest, Node n) override;
/** Check at effort e */
- void check(Effort e);
+ void check(Effort e) override;
/** needs check last effort */
- bool needsCheckLastEffort();
+ bool needsCheckLastEffort() override;
/** Conflict when merging two constants */
void conflict(TNode a, TNode b);
/** called when a new equivalence class is created */
/** called when two equivalence classes are made disequal */
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
/** get preprocess */
- StringsPreprocess * getPreprocess() { return &d_preproc; }
-protected:
+ StringsPreprocess* getPreprocess() { return &d_preproc; }
+
+ protected:
/** compute care graph */
- void computeCareGraph();
+ void computeCareGraph() override;
- //do pending merges
+ // do pending merges
void assertPendingFact(Node atom, bool polarity, Node exp);
void doPendingFacts();
void doPendingLemmas();
bool hasProcessed();
- void addToExplanation( Node a, Node b, std::vector< Node >& exp );
- void addToExplanation( Node lit, std::vector< Node >& exp );
-
- //register term
- void registerTerm( Node n, int effort );
- //send lemma
- void sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma = false );
- void sendInference( std::vector< Node >& exp, Node eq, const char * c, bool asLemma = false );
- void sendLemma( Node ant, Node conc, const char * c );
- void sendInfer( Node eq_exp, Node eq, const char * c );
+ void addToExplanation(Node a, Node b, std::vector<Node>& exp);
+ void addToExplanation(Node lit, std::vector<Node>& exp);
+
+ // register term
+ void registerTerm(Node n, int effort);
+ // send lemma
+ void sendInference(std::vector<Node>& exp,
+ std::vector<Node>& exp_n,
+ Node eq,
+ const char* c,
+ bool asLemma = false);
+ void sendInference(std::vector<Node>& exp,
+ Node eq,
+ const char* c,
+ bool asLemma = false);
+ void sendLemma(Node ant, Node conc, const char* c);
+ void sendInfer(Node eq_exp, Node eq, const char* c);
bool sendSplit(Node a, Node b, const char* c, bool preq = true);
- void sendLengthLemma( Node n );
+ void sendLengthLemma(Node n);
/** mkConcat **/
- inline Node mkConcat( Node n1, Node n2 );
- inline Node mkConcat( Node n1, Node n2, Node n3 );
- inline Node mkConcat( const std::vector< Node >& c );
- inline Node mkLength( Node n );
- //mkSkolem
- enum {
+ inline Node mkConcat(Node n1, Node n2);
+ inline Node mkConcat(Node n1, Node n2, Node n3);
+ inline Node mkConcat(const std::vector<Node>& c);
+ inline Node mkLength(Node n);
+ // mkSkolem
+ enum
+ {
sk_id_c_spt,
sk_id_vc_spt,
sk_id_vc_bin_spt,
- sk_id_v_spt,
+ sk_id_v_spt,
sk_id_c_spt_rev,
sk_id_vc_spt_rev,
sk_id_vc_bin_spt_rev,
sk_id_deq_y,
sk_id_deq_z,
};
- std::map< Node, std::map< Node, std::map< int, Node > > > d_skolem_cache;
- Node mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit = 0 );
- inline Node mkSkolemS(const char * c, int isLenSplit = 0);
- void registerNonEmptySkolem( Node sk );
- //inline Node mkSkolemI(const char * c);
+ std::map<Node, std::map<Node, std::map<int, Node> > > d_skolem_cache;
+ Node mkSkolemCached(
+ Node a, Node b, int id, const char* c, int isLenSplit = 0);
+ inline Node mkSkolemS(const char* c, int isLenSplit = 0);
+ void registerNonEmptySkolem(Node sk);
+ // inline Node mkSkolemI(const char * c);
/** mkExplain **/
- Node mkExplain( std::vector< Node >& a );
- Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
+ Node mkExplain(std::vector<Node>& a);
+ Node mkExplain(std::vector<Node>& a, std::vector<Node>& an);
/** mkAnd **/
- Node mkAnd( std::vector< Node >& a );
+ Node mkAnd(std::vector<Node>& a);
/** get concat vector */
- void getConcatVec( Node n, std::vector< Node >& c );
+ void getConcatVec(Node n, std::vector<Node>& c);
- //get equivalence classes
- void getEquivalenceClasses( std::vector< Node >& eqcs );
+ // get equivalence classes
+ void getEquivalenceClasses(std::vector<Node>& eqcs);
- //separate into collections with equal length
- void separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
- void printConcat( std::vector< Node >& n, const char * c );
+ // separate into collections with equal length
+ void separateByLength(std::vector<Node>& n,
+ std::vector<std::vector<Node> >& col,
+ std::vector<Node>& lts);
+ void printConcat(std::vector<Node>& n, const char* c);
- void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc );
+ void inferSubstitutionProxyVars(Node n,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs,
+ std::vector<Node>& unproc);
// Symbolic Regular Expression
-private:
+ private:
// regular expression memberships
NodeList d_regexp_memberships;
NodeSet d_regexp_ucached;
// Finite Model Finding
-private:
+ private:
NodeSet d_input_vars;
context::CDO< Node > d_input_var_lsum;
context::CDHashMap< int, Node > d_cardinality_lits;
context::CDO< int > d_curr_cardinality;
-public:
+
+ public:
//for finite model finding
- Node getNextDecisionRequest( unsigned& priority );
- //ppRewrite
- Node ppRewrite(TNode atom);
-public:
-/** statistics class */
+ Node getNextDecisionRequest(unsigned& priority) override;
+ // ppRewrite
+ Node ppRewrite(TNode atom) override;
+
+ public:
+ /** statistics class */
class Statistics {
public:
IntStat d_splits;
*/
Node getValue(TNode n, bool useDontCares = false) const;
/** get comments */
- void getComments(std::ostream& out) const;
+ void getComments(std::ostream& out) const override;
//---------------------------- separation logic
/** set the heap and value sep.nil is equal to */
void setHeapModel(Node h, Node neq);
/** get the heap and value sep.nil is equal to */
- bool getHeapModel(Expr& h, Expr& neq) const;
+ bool getHeapModel(Expr& h, Expr& neq) const override;
//---------------------------- end separation logic
/** get the representative set object */
/** get the representative set object (FIXME: remove this, see #1199) */
RepSet* getRepSetPtr() { return &d_rep_set; }
/** return whether this node is a don't-care */
- bool isDontCare(Expr expr) const;
+ bool isDontCare(Expr expr) const override;
/** get value function for Exprs. */
- Expr getValue( Expr expr ) const;
+ Expr getValue(Expr expr) const override;
/** get cardinality for sort */
- Cardinality getCardinality( Type t ) const;
+ Cardinality getCardinality(Type t) const override;
/** print representative debug function */
void printRepresentativeDebug( const char* c, Node r );
/** print representative function */
~TheoryUF();
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
- void finishInit();
+ void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+ void finishInit() override;
- void check(Effort);
- Node expandDefinition(LogicRequest &logicRequest, Node node);
- void preRegisterTerm(TNode term);
- Node explain(TNode n);
+ void check(Effort) override;
+ Node expandDefinition(LogicRequest& logicRequest, Node node) override;
+ void preRegisterTerm(TNode term) override;
+ Node explain(TNode n) override;
bool collectModelInfo(TheoryModel* m) override;
- void ppStaticLearn(TNode in, NodeBuilder<>& learned);
- void presolve();
+ void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
+ void presolve() override;
- void addSharedTerm(TNode n);
- void computeCareGraph();
+ void addSharedTerm(TNode n) override;
+ void computeCareGraph() override;
- void propagate(Effort effort);
- Node getNextDecisionRequest( unsigned& priority );
+ void propagate(Effort effort) override;
+ Node getNextDecisionRequest(unsigned& priority) override;
- EqualityStatus getEqualityStatus(TNode a, TNode b);
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
- std::string identify() const {
- return "THEORY_UF";
- }
+ std::string identify() const override { return "THEORY_UF"; }
- eq::EqualityEngine* getEqualityEngine() {
- return &d_equalityEngine;
- }
+ eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
StrongSolverTheoryUF* getStrongSolver() {
return d_thss;
projects / cvc5.git / commitdiff