summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/proof/proof_rule.cpp5
-rw-r--r--src/proof/proof_rule.h24
-rw-r--r--src/theory/arith/constraint.cpp7
-rw-r--r--src/theory/arith/pp_rewrite_eq.cpp5
-rw-r--r--src/theory/arith/proof_checker.cpp22
-rw-r--r--src/theory/arrays/inference_manager.cpp7
-rw-r--r--src/theory/arrays/proof_checker.cpp9
-rw-r--r--src/theory/arrays/theory_arrays.cpp3
-rw-r--r--src/theory/datatypes/infer_proof_cons.cpp4
-rw-r--r--src/theory/datatypes/proof_checker.cpp8
-rw-r--r--src/theory/strings/infer_proof_cons.cpp11
-rw-r--r--src/theory/strings/proof_checker.cpp9
12 files changed, 26 insertions, 88 deletions
diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp
index 008b0dc6f..286396523 100644
--- a/src/proof/proof_rule.cpp
+++ b/src/proof/proof_rule.cpp
@@ -79,7 +79,6 @@ const char* toString(PfRule id)
case PfRule::ITE_ELIM2: return "ITE_ELIM2";
case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1";
case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2";
- //================================================= De Morgan rules
case PfRule::NOT_AND: return "NOT_AND";
//================================================= CNF rules
case PfRule::CNF_AND_POS: return "CNF_AND_POS";
@@ -120,7 +119,6 @@ const char* toString(PfRule id)
return "ARRAYS_READ_OVER_WRITE_CONTRA";
case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
case PfRule::ARRAYS_EXT: return "ARRAYS_EXT";
- case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST";
case PfRule::ARRAYS_EQ_RANGE_EXPAND: return "ARRAYS_EQ_RANGE_EXPAND";
//================================================= Bit-Vector rules
case PfRule::BV_BITBLAST: return "BV_BITBLAST";
@@ -132,7 +130,6 @@ const char* toString(PfRule id)
case PfRule::DT_COLLAPSE: return "DT_COLLAPSE";
case PfRule::DT_SPLIT: return "DT_SPLIT";
case PfRule::DT_CLASH: return "DT_CLASH";
- case PfRule::DT_TRUST: return "DT_TRUST";
//================================================= Quantifiers rules
case PfRule::SKOLEM_INTRO: return "SKOLEM_INTRO";
case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
@@ -160,7 +157,6 @@ const char* toString(PfRule id)
case PfRule::RE_ELIM: return "RE_ELIM";
case PfRule::STRING_CODE_INJ: return "STRING_CODE_INJ";
case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ";
- case PfRule::STRING_TRUST: return "STRING_TRUST";
//================================================= Arith rules
case PfRule::MACRO_ARITH_SCALE_SUM_UB:
return "ARITH_SCALE_SUM_UPPER_BOUNDS";
@@ -168,7 +164,6 @@ const char* toString(PfRule id)
case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY";
case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB";
case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB";
- case PfRule::INT_TRUST: return "INT_TRUST";
case PfRule::ARITH_MULT_SIGN: return "ARITH_MULT_SIGN";
case PfRule::ARITH_MULT_POS: return "ARITH_MULT_POS";
case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG";
diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index 78e773bdc..7a3ce6882 100644
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -722,12 +722,6 @@ enum class PfRule : uint32_t
// (forall ((x T))
// (=> (and (<= i x) (<= x j)) (= (select a x) (select b x)))))
ARRAYS_EQ_RANGE_EXPAND,
- // ======== Array Trust
- // Children: (P1 ... Pn)
- // Arguments: (F)
- // ---------------------
- // Conclusion: F
- ARRAYS_TRUST,
//================================================= Bit-Vector rules
// Note: bitblast() represents the result of the bit-blasted term as a
@@ -800,12 +794,6 @@ enum class PfRule : uint32_t
// Conclusion: false
// for i != j.
DT_CLASH,
- // ======== Datatype Trust
- // Children: (P1 ... Pn)
- // Arguments: (F)
- // ---------------------
- // Conclusion: F
- DT_TRUST,
//================================================= Quantifiers rules
// ======== Skolem intro
@@ -1082,12 +1070,6 @@ enum class PfRule : uint32_t
// Also applies to the case where (seq.unit y) is a constant sequence
// of length one.
STRING_SEQ_UNIT_INJ,
- // ======== String Trust
- // Children: none
- // Arguments: (Q)
- // ---------------------
- // Conclusion: (Q)
- STRING_TRUST,
//================================================= Arithmetic rules
// ======== Adding Inequalities
@@ -1152,12 +1134,6 @@ enum class PfRule : uint32_t
// ---------------------
// Conclusion: arith::OperatorElim::getAxiomFor(t)
ARITH_OP_ELIM_AXIOM,
- // ======== Int Trust
- // Children: (P1 ... Pn)
- // Arguments: (Q)
- // ---------------------
- // Conclusion: (Q)
- INT_TRUST,
//======== Multiplication sign inference
// Children: none
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index d8fc1c578..03db36bb5 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -29,6 +29,7 @@
#include "theory/arith/congruence_manager.h"
#include "theory/arith/normal_form.h"
#include "theory/arith/partial_model.h"
+#include "theory/builtin/proof_checker.h"
#include "theory/rewriter.h"
using namespace std;
@@ -1820,9 +1821,11 @@ std::shared_ptr<ProofNode> Constraint::externalExplain(
}
case ArithProofType::IntHoleAP:
{
- pf = pnm->mkNode(PfRule::INT_TRUST,
+ Node t =
+ builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH);
+ pf = pnm->mkNode(PfRule::THEORY_INFERENCE,
children,
- {getProofLiteral()},
+ {getProofLiteral(), t},
getProofLiteral());
break;
}
diff --git a/src/theory/arith/pp_rewrite_eq.cpp b/src/theory/arith/pp_rewrite_eq.cpp
index 45f972038..0f4d97b4d 100644
--- a/src/theory/arith/pp_rewrite_eq.cpp
+++ b/src/theory/arith/pp_rewrite_eq.cpp
@@ -16,6 +16,7 @@
#include "theory/arith/pp_rewrite_eq.h"
#include "options/arith_options.h"
+#include "theory/builtin/proof_checker.h"
#include "theory/rewriter.h"
namespace cvc5 {
@@ -44,10 +45,12 @@ TrustNode PreprocessRewriteEq::ppRewriteEq(TNode atom)
// don't need to rewrite terms since rewritten is not a non-standard op
if (proofsEnabled())
{
+ Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH);
return d_ppPfGen.mkTrustedRewrite(
atom,
rewritten,
- d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)}));
+ d_pnm->mkNode(
+ PfRule::THEORY_INFERENCE, {}, {atom.eqNode(rewritten), t}));
}
return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
}
diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp
index 4e25ae76b..58de8e391 100644
--- a/src/theory/arith/proof_checker.cpp
+++ b/src/theory/arith/proof_checker.cpp
@@ -36,11 +36,8 @@ void ArithProofRuleChecker::registerTo(ProofChecker* pc)
pc->registerChecker(PfRule::INT_TIGHT_UB, this);
pc->registerChecker(PfRule::INT_TIGHT_LB, this);
pc->registerChecker(PfRule::ARITH_OP_ELIM_AXIOM, this);
-
pc->registerChecker(PfRule::ARITH_MULT_POS, this);
pc->registerChecker(PfRule::ARITH_MULT_NEG, this);
- // trusted rules
- pc->registerTrustedChecker(PfRule::INT_TRUST, this, 2);
}
Node ArithProofRuleChecker::checkInternal(PfRule id,
@@ -340,25 +337,6 @@ Node ArithProofRuleChecker::checkInternal(PfRule id,
}
// Check that all have the same constant:
}
- case PfRule::INT_TRUST:
- {
- if (Debug.isOn("arith::pf::check::trust"))
- {
- Debug("arith::pf::check::trust") << "Arith PfRule:" << id << std::endl;
- Debug("arith::pf::check::trust") << " children: " << std::endl;
- for (const auto& c : children)
- {
- Debug("arith::pf::check::trust") << " * " << c << std::endl;
- }
- Debug("arith::pf::check::trust") << " args:" << std::endl;
- for (const auto& c : args)
- {
- Debug("arith::pf::check::trust") << " * " << c << std::endl;
- }
- }
- Assert(args.size() == 1);
- return args[0];
- }
case PfRule::ARITH_OP_ELIM_AXIOM:
{
Assert(children.empty());
diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index fc3f67cf0..2949cf105 100644
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -16,6 +16,7 @@
#include "theory/arrays/inference_manager.h"
#include "options/smt_options.h"
+#include "theory/builtin/proof_checker.h"
#include "theory/theory.h"
#include "theory/theory_state.h"
#include "theory/uf/equality_engine.h"
@@ -116,13 +117,15 @@ void InferenceManager::convert(PfRule& id,
break;
case PfRule::ARRAYS_EXT: children.push_back(exp); break;
default:
- if (id != PfRule::ARRAYS_TRUST)
+ if (id != PfRule::THEORY_INFERENCE)
{
Assert(false) << "Unknown rule " << id << "\n";
}
children.push_back(exp);
args.push_back(conc);
- id = PfRule::ARRAYS_TRUST;
+ args.push_back(
+ builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARRAYS));
+ id = PfRule::THEORY_INFERENCE;
break;
}
}
diff --git a/src/theory/arrays/proof_checker.cpp b/src/theory/arrays/proof_checker.cpp
index 6d546d746..557a43a02 100644
--- a/src/theory/arrays/proof_checker.cpp
+++ b/src/theory/arrays/proof_checker.cpp
@@ -31,8 +31,6 @@ void ArraysProofRuleChecker::registerTo(ProofChecker* pc)
pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_1, this);
pc->registerChecker(PfRule::ARRAYS_EXT, this);
pc->registerChecker(PfRule::ARRAYS_EQ_RANGE_EXPAND, this);
- // trusted rules
- pc->registerTrustedChecker(PfRule::ARRAYS_TRUST, this, 2);
}
Node ArraysProofRuleChecker::checkInternal(PfRule id,
@@ -111,13 +109,6 @@ Node ArraysProofRuleChecker::checkInternal(PfRule id,
Node expandedEqRange = TheoryArraysRewriter::expandEqRange(args[0]);
return args[0].eqNode(expandedEqRange);
}
- if (id == PfRule::ARRAYS_TRUST)
- {
- // "trusted" rules
- Assert(!args.empty());
- Assert(args[0].getType().isBoolean());
- return args[0];
- }
// no rule
return Node::null();
}
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 1a6dfedbb..0f0d24cde 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1671,11 +1671,12 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
{
preRegisterTermInternal(selConst);
}
+ // not currently supported in proofs, use THEORY_INFERENCE
d_im.assertInference(selConst.eqNode(defValue),
true,
InferenceId::ARRAYS_CONST_ARRAY_DEFAULT,
d_true,
- PfRule::ARRAYS_TRUST);
+ PfRule::THEORY_INFERENCE);
}
const CTNodeList* stores = d_infoMap.getStores(a);
diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index a4323a1d0..afbfd16c1 100644
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -17,6 +17,7 @@
#include "proof/proof.h"
#include "proof/proof_checker.h"
+#include "theory/builtin/proof_checker.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/model_manager.h"
#include "theory/rewriter.h"
@@ -243,7 +244,8 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
{
// failed to reconstruct, add trust
Trace("dt-ipc") << "...failed " << infer << std::endl;
- cdp->addStep(conc, PfRule::DT_TRUST, expv, {conc});
+ Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_DATATYPES);
+ cdp->addStep(conc, PfRule::THEORY_INFERENCE, expv, {conc, t});
}
else
{
diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp
index 77f9a4c27..23ca26a1f 100644
--- a/src/theory/datatypes/proof_checker.cpp
+++ b/src/theory/datatypes/proof_checker.cpp
@@ -30,8 +30,6 @@ void DatatypesProofRuleChecker::registerTo(ProofChecker* pc)
pc->registerChecker(PfRule::DT_COLLAPSE, this);
pc->registerChecker(PfRule::DT_SPLIT, this);
pc->registerChecker(PfRule::DT_CLASH, this);
- // trusted rules
- pc->registerTrustedChecker(PfRule::DT_TRUST, this, 2);
}
Node DatatypesProofRuleChecker::checkInternal(PfRule id,
@@ -122,12 +120,6 @@ Node DatatypesProofRuleChecker::checkInternal(PfRule id,
}
return nm->mkConst(false);
}
- else if (id == PfRule::DT_TRUST)
- {
- Assert(!args.empty());
- Assert(args[0].getType().isBoolean());
- return args[0];
- }
// no rule
return Node::null();
}
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index b8c0a851c..f48d29416 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -541,7 +541,7 @@ void InferProofCons::convert(InferenceId infer,
if (conc.getKind() != OR)
{
// This should never happen. If it does, we resort to using
- // STRING_TRUST below (in production mode).
+ // THEORY_INFERENCE below (in production mode).
Assert(false) << "Expected OR conclusion for " << infer;
}
else
@@ -876,7 +876,7 @@ void InferProofCons::convert(InferenceId infer,
case InferenceId::STRINGS_CTN_TRANS:
case InferenceId::STRINGS_CTN_DECOMPOSE:
default:
- // do nothing, these will be converted to STRING_TRUST below since the
+ // do nothing, these will be converted to THEORY_INFERENCE below since the
// rule is unknown.
break;
}
@@ -925,11 +925,14 @@ void InferProofCons::convert(InferenceId infer,
Trace("strings-ipc-fail") << " e: " << ec << std::endl;
}
}
- // untrustworthy conversion, the argument of STRING_TRUST is its conclusion
+ // untrustworthy conversion, the argument of THEORY_INFERENCE is its
+ // conclusion
ps.d_args.clear();
ps.d_args.push_back(conc);
+ Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_STRINGS);
+ ps.d_args.push_back(t);
// use the trust rule
- ps.d_rule = PfRule::STRING_TRUST;
+ ps.d_rule = PfRule::THEORY_INFERENCE;
// add to stats
d_statistics.d_inferencesNoPf << infer;
}
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index 36b42f296..5a4008724 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -53,8 +53,6 @@ void StringProofRuleChecker::registerTo(ProofChecker* pc)
pc->registerChecker(PfRule::RE_ELIM, this);
pc->registerChecker(PfRule::STRING_CODE_INJ, this);
pc->registerChecker(PfRule::STRING_SEQ_UNIT_INJ, this);
- // trusted rules
- pc->registerTrustedChecker(PfRule::STRING_TRUST, this, 2);
}
Node StringProofRuleChecker::checkInternal(PfRule id,
@@ -506,13 +504,6 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
AlwaysAssert(t[0].getType() == t[1].getType());
return t[0].eqNode(t[1]);
}
- else if (id == PfRule::STRING_TRUST)
- {
- // "trusted" rules
- Assert(!args.empty());
- Assert(args[0].getType().isBoolean());
- return args[0];
- }
return Node::null();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback