Each theory has its own proof checker, responsible for checking the rules pertaining to that theory. The main proof checker uses these specialized checkers. Previously the main proof checker (of the proof node manager used across the SMT solver) was connected to these theory proof checkers during initialization of the theory. This commit adds an interface to the theories for retrieving its proof checker (analogous to how one retrieves the rewriter of a theory) which is used by a new method in the theory engine to register a theory proof checker to a given proof checker according to a theory id.
This is in preparation for the new unsat cores based on proofs.
{
theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id);
}
-
+ // Add the proof checkers for each theory
+ if (d_pnm)
+ {
+ d_theoryEngine->initializeProofChecker(d_pnm->getChecker());
+ }
Trace("smt-debug") << "Making prop engine..." << std::endl;
/* force destruction of referenced PropEngine to enforce that statistics
* are unregistered by the obsolete PropEngine object before registered
#include "theory/arith/theory_arith.h"
+#include "expr/proof_checker.h"
#include "expr/proof_rule.h"
#include "options/smt_options.h"
#include "smt/smt_statistics_registry.h"
TheoryRewriter* TheoryArith::getTheoryRewriter() { return &d_rewriter; }
+ProofRuleChecker* TheoryArith::getProofChecker()
+{
+ return d_internal->getProofChecker();
+}
+
bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi)
{
return d_internal->needsEqualityEngine(esi);
//--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
/**
* Returns true if this theory needs an equality engine, which is assigned
* to it (d_equalityEngine) by the equality engine manager during
d_previousStatus(Result::SAT_UNKNOWN),
d_statistics()
{
- ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
- if (pc != nullptr)
- {
- d_checker.registerTo(pc);
- }
}
TheoryArithPrivate::~TheoryArithPrivate(){
}
}
+ArithProofRuleChecker* TheoryArithPrivate::getProofChecker()
+{
+ return &d_checker;
+}
+
// InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const
// inferbounds::InferBoundAlgorithm& param){
// Assert(param.findUpperBound());
// inline void raiseConflict(const ConstraintCPVec& cv){
// d_conflicts.push_back(cv);
// }
-
+
// void raiseConflict(ConstraintCP a, ConstraintCP b);
// void raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c);
*/
bool foundNonlinear() const;
+ /** get the proof checker of this theory */
+ ArithProofRuleChecker* getProofChecker();
+
private:
/** The constant zero. */
DeltaRational d_DELTA_ZERO;
static ConstraintCP vectorToIntHoleConflict(const ConstraintCPVec& conflict);
static void intHoleConflictToVector(ConstraintCP conflicting, ConstraintCPVec& conflict);
-
+
// Returns true if the node contains a literal
// that is an arithmetic literal and is not a sat literal
// No caching is done so this should likely only
d_ppEqualityEngine.addFunctionKind(kind::SELECT);
d_ppEqualityEngine.addFunctionKind(kind::STORE);
- ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
- if (pc != nullptr)
- {
- d_pchecker.registerTo(pc);
- }
// indicate we are using the default theory state object, and the arrays
// inference manager
d_theoryState = &d_state;
TheoryRewriter* TheoryArrays::getTheoryRewriter() { return &d_rewriter; }
+ProofRuleChecker* TheoryArrays::getProofChecker() { return &d_checker; }
+
bool TheoryArrays::needsEqualityEngine(EeSetupInfo& esi)
{
esi.d_notify = &d_notify;
//--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
/**
* Returns true if we need an equality engine. If so, we initialize the
* information regarding how it should be setup. For details, see the
NotifyClass d_notify;
/** The proof checker */
- ArraysProofRuleChecker d_pchecker;
+ ArraysProofRuleChecker d_checker;
/** Conflict when merging constants */
void conflict(TNode a, TNode b);
#include "theory/bags/theory_bags.h"
+#include "expr/proof_checker.h"
#include "smt/logic_exception.h"
#include "theory/bags/normal_form.h"
#include "theory/rewriter.h"
TheoryRewriter* TheoryBags::getTheoryRewriter() { return &d_rewriter; }
+ProofRuleChecker* TheoryBags::getProofChecker() { return nullptr; }
+
bool TheoryBags::needsEqualityEngine(EeSetupInfo& esi)
{
esi.d_notify = &d_notify;
//--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
/**
* Returns true if we need an equality engine. If so, we initialize the
* information regarding how it should be setup. For details, see the
#include "theory/valuation.h"
#include "util/hash.h"
-using namespace std;
-
namespace cvc5 {
namespace theory {
namespace booleans {
ProofNodeManager* pnm)
: Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, pnm)
{
- ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
- if (pc != nullptr)
- {
- // add checkers
- d_bProofChecker.registerTo(pc);
- }
}
Theory::PPAssertStatus TheoryBool::ppAssert(
return Theory::ppAssert(tin, outSubstitutions);
}
+TheoryRewriter* TheoryBool::getTheoryRewriter() { return &d_rewriter; }
+
+ProofRuleChecker* TheoryBool::getProofChecker() { return &d_checker; }
+
+std::string TheoryBool::identify() const { return std::string("TheoryBool"); }
+
} // namespace booleans
} // namespace theory
} // namespace cvc5
const LogicInfo& logicInfo,
ProofNodeManager* pnm = nullptr);
- TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
+ /** get the official theory rewriter of this theory */
+ TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
PPAssertStatus ppAssert(TrustNode tin,
TrustSubstitutionMap& outSubstitutions) override;
- std::string identify() const override { return std::string("TheoryBool"); }
+ std::string identify() const override;
private:
/** The theory rewriter for this theory. */
TheoryBoolRewriter d_rewriter;
/** Proof rule checker */
- BoolProofRuleChecker d_bProofChecker;
+ BoolProofRuleChecker d_checker;
};/* class TheoryBool */
} // namespace booleans
#include "theory/theory_model.h"
#include "theory/valuation.h"
-using namespace std;
-
namespace cvc5 {
namespace theory {
namespace builtin {
ProofNodeManager* pnm)
: Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, pnm)
{
- ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
- if (pc != nullptr)
- {
- // add checkers
- d_bProofChecker.registerTo(pc);
- }
}
+TheoryRewriter* TheoryBuiltin::getTheoryRewriter() { return &d_rewriter; }
+
+ProofRuleChecker* TheoryBuiltin::getProofChecker() { return &d_checker; }
+
std::string TheoryBuiltin::identify() const
{
return std::string("TheoryBuiltin");
const LogicInfo& logicInfo,
ProofNodeManager* pnm = nullptr);
- TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
+ /** get the official theory rewriter of this theory */
+ TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
std::string identify() const override;
/** The theory rewriter for this theory. */
TheoryBuiltinRewriter d_rewriter;
/** Proof rule checker */
- BuiltinProofRuleChecker d_bProofChecker;
+ BuiltinProofRuleChecker d_checker;
}; /* class TheoryBuiltin */
} // namespace builtin
d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
: nullptr)
{
- if (pnm != nullptr)
- {
- d_bvProofChecker.registerTo(pnm->getChecker());
- }
}
void BVSolverSimple::addBBLemma(TNode fact)
return d_bitblaster->collectModelValues(m, termSet);
}
+BVProofRuleChecker* BVSolverSimple::getProofChecker() { return &d_checker; }
+
} // namespace bv
} // namespace theory
} // namespace cvc5
#include "theory/eager_proof_generator.h"
namespace cvc5 {
-
namespace theory {
namespace bv {
bool collectModelValues(TheoryModel* m,
const std::set<Node>& termSet) override;
+ /** get the proof checker of this theory */
+ BVProofRuleChecker* getProofChecker();
+
private:
/**
* Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the
/** Proof generator that manages proofs for lemmas generated by this class. */
std::unique_ptr<EagerProofGenerator> d_epg;
-
- BVProofRuleChecker d_bvProofChecker;
+ /** Proof rule checker */
+ BVProofRuleChecker d_checker;
};
} // namespace bv
#include "theory/bv/theory_bv.h"
+#include "expr/proof_checker.h"
#include "options/bv_options.h"
#include "options/smt_options.h"
#include "theory/bv/bv_solver_bitblast.h"
TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
+ProofRuleChecker* TheoryBV::getProofChecker()
+{
+ if (options::bvSolver() == options::BVSolver::SIMPLE)
+ {
+ return static_cast<BVSolverSimple*>(d_internal.get())->getProofChecker();
+ }
+ return nullptr;
+}
+
bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
{
bool need_ee = d_internal->needsEqualityEngine(esi);
#include "theory/theory_state.h"
namespace cvc5 {
+
+class ProofRuleChecker;
+
namespace theory {
namespace bv {
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
/**
* Returns true if we need an equality engine. If so, we initialize the
// indicate we are using the default theory state object
d_theoryState = &d_state;
d_inferManager = &d_im;
-
- ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
- if (pc != nullptr)
- {
- // add checkers
- d_pchecker.registerTo(pc);
- }
}
TheoryDatatypes::~TheoryDatatypes() {
TheoryRewriter* TheoryDatatypes::getTheoryRewriter() { return &d_rewriter; }
+ProofRuleChecker* TheoryDatatypes::getProofChecker() { return &d_checker; }
+
bool TheoryDatatypes::needsEqualityEngine(EeSetupInfo& esi)
{
esi.d_notify = &d_notify;
if( n.getKind()==APPLY_CONSTRUCTOR ){
ei->d_constructor = n;
}
-
+
//add to selectors
d_selector_apps[n] = 0;
-
+
return ei;
}else{
return NULL;
}else{
d_selector_apps_data[n].push_back( s );
}
-
+
eqc->d_selectors = true;
}
if( assertFacts && !eqc->d_constructor.get().isNull() ){
//--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
/**
* Returns true if we need an equality engine. If so, we initialize the
* information regarding how it should be setup. For details, see the
/** The notify class */
NotifyClass d_notify;
/** Proof checker for datatypes */
- DatatypesProofRuleChecker d_pchecker;
+ DatatypesProofRuleChecker d_checker;
};/* class TheoryDatatypes */
} // namespace datatypes
TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; }
+ProofRuleChecker* TheoryFp::getProofChecker() { return nullptr; }
+
bool TheoryFp::needsEqualityEngine(EeSetupInfo& esi)
{
esi.d_notify = &d_notification;
d_im.conflictEqConstantMerge(t1, t2);
}
-
-bool TheoryFp::needsCheckLastEffort()
-{
+bool TheoryFp::needsCheckLastEffort()
+{
// only need to check if we have added to the abstraction map, otherwise
// postCheck below is a no-op.
- return !d_abstractionMap.empty();
+ return !d_abstractionMap.empty();
}
void TheoryFp::postCheck(Effort level)
//--------------------------------- initialization
/** Get the official theory rewriter of this theory. */
TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
/**
* Returns true if we need an equality engine. If so, we initialize the
* information regarding how it should be setup. For details, see the
out.handleUserAttribute( "quant-elim", this );
out.handleUserAttribute( "quant-elim-partial", this );
- ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
- if (pc != nullptr)
- {
- // add the proof rules
- d_qChecker.registerTo(pc);
- }
-
// Finish initializing the term registry by hooking it up to the inference
// manager. This is required due to a cyclic dependency between the term
// database and the instantiate module. Term database needs inference manager
}
TheoryRewriter* TheoryQuantifiers::getTheoryRewriter() { return &d_rewriter; }
+
+ProofRuleChecker* TheoryQuantifiers::getProofChecker() { return &d_checker; }
+
void TheoryQuantifiers::finishInit()
{
// quantifiers are not evaluated in getModelValue
//--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
/** finish initialization */
void finishInit() override;
/** needs equality engine */
/** The theory rewriter for this theory. */
QuantifiersRewriter d_rewriter;
/** The proof rule checker */
- QuantifiersProofRuleChecker d_qChecker;
+ QuantifiersProofRuleChecker d_checker;
/** The quantifiers state */
QuantifiersState d_qstate;
/** The quantifiers registry */
TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; }
+ProofRuleChecker* TheorySep::getProofChecker() { return nullptr; }
+
bool TheorySep::needsEqualityEngine(EeSetupInfo& esi)
{
esi.d_notify = &d_notify;
void TheorySep::postProcessModel( TheoryModel* m ){
Trace("sep-model") << "Printing model for TheorySep..." << std::endl;
-
+
std::vector< Node > sep_children;
Node m_neq;
Node m_heap;
}
//return cardinality
-int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& visited,
- 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 ) {
+int TheorySep::processAssertion(
+ Node n,
+ std::map<int, std::map<Node, int> >& visited,
+ 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)
+{
int index = hasPol ? ( pol ? 1 : -1 ) : 0;
int card = 0;
std::map< Node, int >::iterator it = visited[index].find( n );
registerRefDataTypesAtom(n);
if( hasPol && pol ){
references[index][n].clear();
- references_strict[index][n] = true;
+ references_strict[index][n] = true;
}else{
card = 1;
}
references[index][n].push_back( n[0] );
}
if( hasPol && pol ){
- references_strict[index][n] = true;
+ references_strict[index][n] = true;
}else{
card = 1;
}
}else{
card = it->second;
}
-
+
if( !underSpatial && ( !references[index][n].empty() || card>0 ) ){
TypeNode tn = getReferenceType( n );
Assert(!tn.isNull());
Trace("sep-bound") << "Initialize bounds for " << tn << "..." << std::endl;
unsigned n_emp = 0;
if( d_bound_kind[tn] != bound_invalid ){
- n_emp = d_card_max[tn];
+ n_emp = d_card_max[tn];
}else if( d_type_references[tn].empty() ){
//must include at least one constant TODO: remove?
n_emp = 1;
}
}else{
//break symmetries TODO
-
+
d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references_card[tn].begin(), d_type_references_card[tn].end() );
}
//Assert( !d_type_references_all[tn].empty() );
-
- if( d_bound_kind[tn]!=bound_invalid ){
+
+ if (d_bound_kind[tn] != bound_invalid)
+ {
//construct bound
d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] );
Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl;
}
}
}
-
+
//assert that nil ref is not in base label
Node nr = getNilRef( tn );
Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, n_lbl ).negate();
}
}
-Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model,
- TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind ) {
+Node TheorySep::instantiateLabel(Node n,
+ Node o_lbl,
+ Node lbl,
+ Node lbl_v,
+ std::map<Node, Node>& visited,
+ std::map<Node, Node>& pto_model,
+ TypeNode rtn,
+ std::map<Node, bool>& active_lbl,
+ unsigned ind)
+{
Trace("sep-inst-debug") << "Instantiate label " << n << " " << lbl << " " << lbl_v << std::endl;
if( options::sepMinimalRefine() && lbl!=o_lbl && active_lbl.find( lbl )!=active_lbl.end() ){
Trace("sep-inst") << "...do not instantiate " << o_lbl << " since it has an active sublabel " << lbl << std::endl;
for( unsigned i=0; i<children.size(); i++ ){
std::vector< Node > tchildren;
Node mval = mvals[i];
- tchildren.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, mval, lbl ) );
+ tchildren.push_back(
+ NodeManager::currentNM()->mkNode(kind::SUBSET, mval, lbl));
tchildren.push_back( children[i] );
std::vector< Node > rem_children;
for( unsigned j=0; j<children.size(); j++ ){
Node sub_lbl_0 = d_label_map[n][lbl][0];
Node lbl_mval_0 = d_label_model[sub_lbl_0].getValue( rtn );
wchildren.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval_0, lbl ).eqNode( empSet ).negate() );
-
+
//return the lemma
wchildren.push_back( children[0].negate() );
wchildren.push_back( children[1] );
/** True node for predicates = false */
Node d_false;
-
+
//whether bounds have been initialized
bool d_bounds_init;
Node mkAnd( std::vector< TNode >& assumptions );
- int processAssertion( Node n, std::map< int, std::map< Node, int > >& visited,
- 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 );
+ int processAssertion(
+ Node n,
+ std::map<int, std::map<Node, int> >& visited,
+ 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:
TheorySep(context::Context* c,
//--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
/**
* Returns true if we need an equality engine. If so, we initialize the
* information regarding how it should be setup. For details, see the
bound_invalid,
};
std::map< TypeNode, unsigned > d_bound_kind;
-
+
std::map< TypeNode, std::vector< Node > > d_type_references_card;
std::map< Node, unsigned > d_type_ref_card_id;
std::map< TypeNode, std::vector< Node > > d_type_references_all;
void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity );
void mergePto( Node p1, Node p2 );
void computeLabelModel( Node lbl );
- Node instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model,
- TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind = 0 );
+ Node instantiateLabel(Node n,
+ Node o_lbl,
+ Node lbl,
+ Node lbl_v,
+ std::map<Node, Node>& visited,
+ std::map<Node, Node>& pto_model,
+ TypeNode rtn,
+ std::map<Node, bool>& active_lbl,
+ unsigned ind = 0);
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 );
return d_internal->getTheoryRewriter();
}
+ProofRuleChecker* TheorySets::getProofChecker() { return nullptr; }
+
bool TheorySets::needsEqualityEngine(EeSetupInfo& esi)
{
esi.d_notify = &d_notify;
//--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
/**
* Returns true if we need an equality engine. If so, we initialize the
* information regarding how it should be setup. For details, see the
void eqNotifyNewClass(TNode t) override;
void eqNotifyMerge(TNode t1, TNode t2) override;
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
-
+
private:
TheorySetsPrivate& d_theory;
};
// set up the extended function callback
d_extTheoryCb.d_esolver = &d_esolver;
- ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
- if (pc != nullptr)
- {
- // add checkers
- d_sProofChecker.registerTo(pc);
- }
// use the state object as the official theory state
d_theoryState = &d_state;
// use the inference manager as the official inference manager
TheoryRewriter* TheoryStrings::getTheoryRewriter() { return &d_rewriter; }
+ProofRuleChecker* TheoryStrings::getProofChecker() { return &d_checker; }
+
bool TheoryStrings::needsEqualityEngine(EeSetupInfo& esi)
{
esi.d_notify = &d_notify;
//--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
/**
* Returns true if we need an equality engine. If so, we initialize the
* information regarding how it should be setup. For details, see the
/** The theory rewriter for this theory. */
StringsRewriter d_rewriter;
/** The proof rule checker */
- StringProofRuleChecker d_sProofChecker;
+ StringProofRuleChecker d_checker;
/**
* The base solver, responsible for reasoning about congruent terms and
* inferring constants for equivalence classes.
class ProofNodeManager;
class TheoryEngine;
+class ProofRuleChecker;
namespace theory {
* @return The theory rewriter associated with this theory.
*/
virtual TheoryRewriter* getTheoryRewriter() = 0;
+ /**
+ * @return The proof checker associated with this theory.
+ */
+ virtual ProofRuleChecker* getProofChecker() = 0;
/**
* Returns true if this theory needs an equality engine for checking
* satisfiability.
#include "expr/lazy_proof.h"
#include "expr/node_builder.h"
#include "expr/node_visitor.h"
+#include "expr/proof_checker.h"
#include "expr/proof_ensure_closed.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
d_resourceManager->spendResource(r);
}
+void TheoryEngine::initializeProofChecker(ProofChecker* pc)
+{
+ for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
+ ++id)
+ {
+ ProofRuleChecker* prc = d_theoryTable[id]->getProofChecker();
+ if (prc)
+ {
+ prc->registerTo(pc);
+ }
+ }
+}
+
} // namespace cvc5
class ResourceManager;
class OutputManager;
class TheoryEngineProofGenerator;
+class ProofChecker;
/**
* A pair of a theory and a node. This is used to mark the flow of
theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
}
+ /** Register theory proof rule checkers to the given proof checker */
+ void initializeProofChecker(ProofChecker* pc);
+
void setPropEngine(prop::PropEngine* propEngine)
{
d_propEngine = propEngine;
d_notify(d_im, *this)
{
d_true = NodeManager::currentNM()->mkConst( true );
-
- ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
- if (pc != nullptr)
- {
- d_ufProofChecker.registerTo(pc);
- }
// indicate we are using the default theory state and inference managers
d_theoryState = &d_state;
d_inferManager = &d_im;
TheoryRewriter* TheoryUF::getTheoryRewriter() { return &d_rewriter; }
+ProofRuleChecker* TheoryUF::getProofChecker() { return &d_checker; }
+
bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi)
{
esi.d_notify = &d_notify;
//--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+ /** get the proof checker of this theory */
+ ProofRuleChecker* getProofChecker() override;
/**
* Returns true if we need an equality engine. If so, we initialize the
* information regarding how it should be setup. For details, see the
bool isHigherOrderType(TypeNode tn);
TheoryUfRewriter d_rewriter;
/** Proof rule checker */
- UfProofRuleChecker d_ufProofChecker;
+ UfProofRuleChecker d_checker;
/** A (default) theory state object */
TheoryState d_state;
/** A (default) inference manager */
#include "expr/dtype_cons.h"
#include "expr/node.h"
#include "expr/node_manager.h"
+#include "expr/proof_checker.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "test.h"
/* -------------------------------------------------------------------------- */
-class DymmyTheoryRewriter : public theory::TheoryRewriter
+class DummyTheoryRewriter : public theory::TheoryRewriter
{
public:
theory::RewriteResponse preRewrite(TNode n) override
}
};
+class DummyProofRuleChecker : public ProofRuleChecker
+{
+ public:
+ DummyProofRuleChecker() {}
+ ~DummyProofRuleChecker() {}
+ void registerTo(ProofChecker* pc) override {}
+
+ protected:
+ Node checkInternal(PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args) override
+ {
+ return Node::null();
+ }
+};
+
/** Dummy Theory interface. */
template <theory::TheoryId theoryId>
class DummyTheory : public theory::Theory
}
theory::TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
+ ProofRuleChecker* getProofChecker() override { return &d_checker; }
void registerTerm(TNode n)
{
*/
std::string d_id;
/** The theory rewriter for this theory. */
- DymmyTheoryRewriter d_rewriter;
+ DummyTheoryRewriter d_rewriter;
+ /** The proof checker for this theory. */
+ DummyProofRuleChecker d_checker;
};
/* -------------------------------------------------------------------------- */
projects / cvc5.git / commitdiff