This enables initial proof support in datatypes, which includes connecting the inference-to-proof constructor to the inference manager and making the proper calls to the inference manager using TheoryDatatypes.
theory/datatypes/inference.h
theory/datatypes/inference_manager.cpp
theory/datatypes/inference_manager.h
+ theory/datatypes/infer_proof_cons.cpp
+ theory/datatypes/infer_proof_cons.h
+ theory/datatypes/proof_checker.cpp
+ theory/datatypes/proof_checker.h
theory/datatypes/sygus_datatype_utils.cpp
theory/datatypes/sygus_datatype_utils.h
theory/datatypes/sygus_extension.cpp
// sent as a lemma in addPendingInference below.
if (asLemma || mustCommunicateFact(d_conc, d_exp))
{
- return d_im->processDtInference(d_conc, d_exp, d_id, true);
+ return d_im->processDtLemma(d_conc, d_exp, d_id);
}
- return d_im->processDtInference(d_conc, d_exp, d_id, false);
+ return d_im->processDtFact(d_conc, d_exp, d_id);
}
InferId DatatypesInference::getInferId() const { return d_id; }
INST,
// (or ((_ is C1) t) V ... V ((_ is Cn) t))
SPLIT,
- // (not ((_ is C1) t)) ^ ... [j] ... ^ (not ((_ is Cn) t)) => ((_ is Ci) t)
+ // (not ((_ is C1) t)) ^ ... [j] ... ^ (not ((_ is Cn) t)) => ((_ is Cj) t)
LABEL_EXH,
// (= t (Ci t1 ... tn)) => (= (sel_j t) rewrite((sel_j (Ci t1 ... tn))))
COLLAPSE_SEL,
CLASH_CONFLICT,
// ((_ is Ci) t) ^ (= t (Cj t1 ... tn)) => false
TESTER_CONFLICT,
- // ((_ is Ci) t) ^ (= t s) ^ ((_ is Cj) s) => false
+ // ((_ is Ci) t) ^ ((_ is Cj) s) ^ (= t s) => false
TESTER_MERGE_CONFLICT,
// bisimilarity for codatatypes
BISIMILAR,
InferenceManager::InferenceManager(Theory& t,
TheoryState& state,
ProofNodeManager* pnm)
- : InferenceManagerBuffered(t, state, nullptr),
+ : InferenceManagerBuffered(t, state, pnm),
d_inferenceLemmas("theory::datatypes::inferenceLemmas"),
- d_inferenceFacts("theory::datatypes::inferenceFacts")
+ d_inferenceFacts("theory::datatypes::inferenceFacts"),
+ d_inferenceConflicts("theory::datatypes::inferenceConflicts"),
+ d_pnm(pnm),
+ d_ipc(pnm == nullptr ? nullptr
+ : new InferProofCons(state.getSatContext(), pnm)),
+ d_lemPg(pnm == nullptr
+ ? nullptr
+ : new EagerProofGenerator(
+ pnm, state.getUserContext(), "datatypes::lemPg"))
{
+ d_false = NodeManager::currentNM()->mkConst(false);
smtStatisticsRegistry()->registerStat(&d_inferenceLemmas);
smtStatisticsRegistry()->registerStat(&d_inferenceFacts);
+ smtStatisticsRegistry()->registerStat(&d_inferenceConflicts);
}
InferenceManager::~InferenceManager()
{
smtStatisticsRegistry()->unregisterStat(&d_inferenceLemmas);
smtStatisticsRegistry()->unregisterStat(&d_inferenceFacts);
+ smtStatisticsRegistry()->unregisterStat(&d_inferenceConflicts);
}
void InferenceManager::addPendingInference(Node conc,
doPendingFacts();
}
+void InferenceManager::sendDtLemma(Node lem,
+ InferId id,
+ LemmaProperty p,
+ bool doCache)
+{
+ if (isProofEnabled())
+ {
+ processDtLemma(lem, Node::null(), id);
+ return;
+ }
+ // otherwise send as a normal lemma
+ if (lemma(lem, p, doCache))
+ {
+ d_inferenceLemmas << id;
+ }
+}
+
+void InferenceManager::sendDtConflict(const std::vector<Node>& conf, InferId id)
+{
+ if (isProofEnabled())
+ {
+ Node exp = NodeManager::currentNM()->mkAnd(conf);
+ prepareDtInference(d_false, exp, id, d_ipc.get());
+ }
+ conflictExp(conf, d_ipc.get());
+ d_inferenceConflicts << id;
+}
+
bool InferenceManager::sendLemmas(const std::vector<Node>& lemmas)
{
bool ret = false;
return ret;
}
-bool InferenceManager::processDtInference(Node conc,
- Node exp,
- InferId id,
- bool asLemma)
+bool InferenceManager::isProofEnabled() const { return d_ipc != nullptr; }
+
+bool InferenceManager::processDtLemma(
+ Node conc, Node exp, InferId id, LemmaProperty p, bool doCache)
{
- Trace("dt-lemma-debug") << "processDtInference : " << conc << " via " << exp
- << " by " << id << ", asLemma = " << asLemma
- << std::endl;
- if (asLemma)
+ // set up a proof constructor
+ std::shared_ptr<InferProofCons> ipcl;
+ if (isProofEnabled())
+ {
+ ipcl = std::make_shared<InferProofCons>(nullptr, d_pnm);
+ }
+ conc = prepareDtInference(conc, exp, id, ipcl.get());
+ // send it as a lemma
+ Node lem;
+ if (!exp.isNull() && !exp.isConst())
+ {
+ lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, conc);
+ }
+ else
+ {
+ lem = conc;
+ }
+ if (isProofEnabled())
{
- // send it as a lemma
- Node lem;
+ // store its proof
+ std::shared_ptr<ProofNode> pbody = ipcl->getProofFor(conc);
+ std::shared_ptr<ProofNode> pn = pbody;
if (!exp.isNull() && !exp.isConst())
{
- lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, conc);
- }
- else
- {
- lem = conc;
+ std::vector<Node> expv;
+ expv.push_back(exp);
+ pn = d_pnm->mkScope(pbody, expv);
}
- if (!lemma(lem))
+ d_lemPg->setProofFor(lem, pn);
+ }
+ // use trusted lemma
+ TrustNode tlem = TrustNode::mkTrustLemma(lem, d_lemPg.get());
+ if (!trustedLemma(tlem))
+ {
+ Trace("dt-lemma-debug") << "...duplicate lemma" << std::endl;
+ return false;
+ }
+ d_inferenceLemmas << id;
+ return true;
+}
+
+bool InferenceManager::processDtFact(Node conc, Node exp, InferId id)
+{
+ conc = prepareDtInference(conc, exp, id, d_ipc.get());
+ // assert the internal fact, which has the same issue as above
+ bool polarity = conc.getKind() != NOT;
+ TNode atom = polarity ? conc : conc[0];
+ if (isProofEnabled())
+ {
+ std::vector<Node> expv;
+ if (!exp.isNull() && !exp.isConst())
{
- Trace("dt-lemma-debug") << "...duplicate lemma" << std::endl;
- return false;
+ expv.push_back(exp);
}
- d_inferenceLemmas << id;
+ assertInternalFact(atom, polarity, expv, d_ipc.get());
}
else
{
- // assert the internal fact, which has the same issue as above
- bool polarity = conc.getKind() != NOT;
- TNode atom = polarity ? conc : conc[0];
+ // use version without proofs
assertInternalFact(atom, polarity, exp);
- d_inferenceFacts << id;
}
+ d_inferenceFacts << id;
return true;
}
+Node InferenceManager::prepareDtInference(Node conc,
+ Node exp,
+ InferId id,
+ InferProofCons* ipc)
+{
+ Trace("dt-lemma-debug") << "prepareDtInference : " << conc << " via " << exp
+ << " by " << id << std::endl;
+ if (conc.getKind() == EQUAL && conc[0].getType().isBoolean())
+ {
+ // must turn (= conc false) into (not conc)
+ conc = Rewriter::rewrite(conc);
+ }
+ if (isProofEnabled())
+ {
+ Assert(ipc != nullptr);
+ // If proofs are enabled, notify the proof constructor.
+ // Notice that we have to reconstruct a datatypes inference here. This is
+ // because the inference in the pending vector may be destroyed as we are
+ // processing this inference, if we triggered to backtrack based on the
+ // call below, since it is a unique pointer.
+ std::shared_ptr<DatatypesInference> di =
+ std::make_shared<DatatypesInference>(this, conc, exp, id);
+ ipc->notifyFact(di);
+ }
+ return conc;
+}
+
} // namespace datatypes
} // namespace theory
} // namespace CVC4
#include "context/cdhashmap.h"
#include "expr/node.h"
+#include "theory/datatypes/infer_proof_cons.h"
#include "theory/datatypes/inference.h"
#include "theory/inference_manager_buffered.h"
#include "util/statistics_registry.h"
* or processed internally.
*/
void process();
+ /**
+ * Send lemma immediately on the output channel
+ */
+ void sendDtLemma(Node lem,
+ InferId i = InferId::NONE,
+ LemmaProperty p = LemmaProperty::NONE,
+ bool doCache = true);
+ /**
+ * Send conflict immediately on the output channel
+ */
+ void sendDtConflict(const std::vector<Node>& conf, InferId i = InferId::NONE);
/**
* Send lemmas with property NONE on the output channel immediately.
* Returns true if any lemma was sent.
bool sendLemmas(const std::vector<Node>& lemmas);
private:
+ /** Are proofs enabled? */
+ bool isProofEnabled() const;
/**
- * Process datatype inference. We send a lemma if asLemma is true, and
- * send an internal fact if asLemma is false.
+ * Process datatype inference as a lemma
+ */
+ bool processDtLemma(Node conc,
+ Node exp,
+ InferId id,
+ LemmaProperty p = LemmaProperty::NONE,
+ bool doCache = true);
+ /**
+ * Process datatype inference as a fact
+ */
+ bool processDtFact(Node conc, Node exp, InferId id);
+ /**
+ * Helper function for the above methods. Returns the conclusion, which
+ * may be modified so that it is compatible with proofs. If proofs are
+ * enabled, it ensures the proof constructor is ready to provide a proof
+ * of (=> exp conc).
+ *
+ * In particular, if conc is a Boolean equality, it is rewritten. This is
+ * to ensure that we do not assert equalities of the form (= t true)
+ * or (= t false) to the equality engine, which have a reserved internal
+ * status for proof generation. If this is not done, then it is possible
+ * to have proofs with missing connections and hence free assumptions.
*/
- bool processDtInference(Node conc, Node exp, InferId id, bool asLemma);
+ Node prepareDtInference(Node conc, Node exp, InferId id, InferProofCons* ipc);
+ /** The false node */
+ Node d_false;
/**
* Counts the number of applications of each type of inference processed by
- * the above method as facts and lemmas.
+ * the above method as facts, lemmas and conflicts.
*/
HistogramStat<InferId> d_inferenceLemmas;
HistogramStat<InferId> d_inferenceFacts;
+ HistogramStat<InferId> d_inferenceConflicts;
+ /** Pointer to the proof node manager */
+ ProofNodeManager* d_pnm;
+ /** The inference to proof converter */
+ std::unique_ptr<InferProofCons> d_ipc;
+ /** An eager proof generator for lemmas */
+ std::unique_ptr<EagerProofGenerator> d_lemPg;
};
} // namespace datatypes
// 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() {
Trace("dt-split") << "*************Split for constructors on " << n << endl;
Node lemma = utils::mkSplit(n, dt);
Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
- d_im.lemma(lemma, LemmaProperty::SEND_ATOMS, false);
+ d_im.sendDtLemma(lemma,
+ InferId::SPLIT,
+ LemmaProperty::SEND_ATOMS,
+ false);
}
if( !options::dtBlastSplits() ){
break;
conf.push_back(unifEq);
Trace("dt-conflict")
<< "CONFLICT: Clash conflict : " << conf << std::endl;
- d_im.conflictExp(conf, nullptr);
+ d_im.sendDtConflict(conf, InferId::CLASH_CONFLICT);
return;
}
else
//conflict because equivalence class contains a constructor
std::vector<Node> conf;
conf.push_back(t);
- conf.push_back(eqc->d_constructor.get().eqNode(t_arg));
+ conf.push_back(t_arg.eqNode(eqc->d_constructor.get()));
Trace("dt-conflict")
<< "CONFLICT: Tester eq conflict " << conf << std::endl;
- d_im.conflictExp(conf, nullptr);
+ d_im.sendDtConflict(conf, InferId::TESTER_CONFLICT);
return;
}else{
makeConflict = true;
conf.push_back(t);
conf.push_back(jt[0].eqNode(t_arg));
Trace("dt-conflict") << "CONFLICT: Tester conflict : " << conf << std::endl;
- d_im.conflictExp(conf, nullptr);
+ d_im.sendDtConflict(conf, InferId::TESTER_MERGE_CONFLICT);
}
}
conf.push_back(c.eqNode(t[0][0]));
Trace("dt-conflict")
<< "CONFLICT: Tester merge eq conflict : " << conf << std::endl;
- d_im.conflictExp(conf, nullptr);
+ d_im.sendDtConflict(conf, InferId::TESTER_CONFLICT);
return;
}
}
Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl;
Node r;
bool wrong = false;
- Node eq_exp = c.eqNode(s[0]);
+ Node eq_exp = s[0].eqNode(c);
if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
Node selector = s.getOperator();
size_t constructorIndex = utils::indexOf(c.getOperator());
if (s != rrs)
{
Node eq = s.eqNode(rrs);
- Node peq = c.eqNode(s[0]);
// Since collapsing selectors may generate new terms, we must send
// this out as a lemma if it is of an external type, or otherwise we
// may ask for the equality status of terms that only datatypes knows
// about, see issue #5344.
bool forceLemma = !s.getType().isDatatype();
Trace("datatypes-infer") << "DtInfer : collapse sel";
- Trace("datatypes-infer") << " : " << eq << " by " << peq << std::endl;
- d_im.addPendingInference(eq, peq, forceLemma, InferId::COLLAPSE_SEL);
+ Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl;
+ d_im.addPendingInference(eq, eq_exp, forceLemma, InferId::COLLAPSE_SEL);
}
}
}
Assert(expl.size() > 0);
Trace("dt-conflict")
<< "CONFLICT: Cycle conflict : " << expl << std::endl;
- d_im.conflictExp(expl, nullptr);
+ d_im.sendDtConflict(expl, InferId::CYCLE);
return;
}
}
if( ncons.getKind()==APPLY_CONSTRUCTOR ) {
Node cc = ncons.getOperator();
cn_cons[part[j]] = ncons;
- if( mkExp ){
+ if (mkExp && c != ncons)
+ {
exp.push_back(c.eqNode(ncons));
}
new_part[cc].push_back( part[j] );
//set current node
for( unsigned k=0; k<split_new_part[j].size(); k++ ){
Node n = split_new_part[j][k];
- cn[n] = getRepresentative( cn_cons[n][cindex] );
- if( mkExp ){
- exp.push_back(cn[n].eqNode(cn_cons[n][cindex]));
+ Node cnc = cn_cons[n][cindex];
+ Node nr = getRepresentative(cnc);
+ cn[n] = nr;
+ if (mkExp && cnc != nr)
+ {
+ exp.push_back(nr.eqNode(cnc));
}
}
std::vector< std::vector< Node > > c_part_out;
#include "expr/node_trie.h"
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/datatypes/inference_manager.h"
+#include "theory/datatypes/proof_checker.h"
#include "theory/datatypes/sygus_extension.h"
#include "theory/theory.h"
#include "theory/theory_eq_notify.h"
InferenceManager d_im;
/** The notify class */
NotifyClass d_notify;
+ /** Proof checker for datatypes */
+ DatatypesProofRuleChecker d_pchecker;
};/* class TheoryDatatypes */
}/* CVC4::theory::datatypes namespace */
projects / cvc5.git / commitdiff