Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Hans-Joerg Schurr, Gereon Kremer
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Arrays inference manager.
14 : : */
15 : :
16 : : #include "theory/arrays/inference_manager.h"
17 : :
18 : : #include "options/smt_options.h"
19 : : #include "proof/trust_id.h"
20 : : #include "theory/builtin/proof_checker.h"
21 : : #include "theory/theory.h"
22 : : #include "theory/theory_state.h"
23 : : #include "theory/uf/equality_engine.h"
24 : :
25 : : using namespace cvc5::internal::kind;
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : : namespace arrays {
30 : :
31 : 47557 : InferenceManager::InferenceManager(Env& env, Theory& t, TheoryState& state)
32 : : : TheoryInferenceManager(env, t, state, "theory::arrays::", false),
33 : 95114 : d_lemmaPg(isProofEnabled() ? new EagerProofGenerator(
34 : 17848 : env, userContext(), "ArrayLemmaProofGenerator")
35 : 65405 : : nullptr)
36 : : {
37 : 47557 : }
38 : :
39 : 19168 : bool InferenceManager::assertInference(
40 : : TNode atom, bool polarity, InferenceId id, TNode reason, ProofRule pfr)
41 : : {
42 [ + - ]: 38336 : Trace("arrays-infer") << "TheoryArrays::assertInference: "
43 [ - - ][ - + ]: 19168 : << (polarity ? Node(atom) : atom.notNode()) << " by "
[ - - ]
44 : 19168 : << reason << "; " << id << std::endl;
45 [ - + ][ - + ]: 19168 : Assert(atom.getKind() == Kind::EQUAL);
[ - - ]
46 : : // if proofs are enabled, we determine which proof rule to add, otherwise
47 : : // we simply assert the internal fact
48 [ + + ]: 19168 : if (isProofEnabled())
49 : : {
50 [ + + ]: 9936 : Node fact = polarity ? Node(atom) : atom.notNode();
51 : 9936 : std::vector<Node> children;
52 : 4968 : std::vector<Node> args;
53 : : // convert to proof rule application
54 : 4968 : convert(pfr, fact, reason, children, args);
55 : 4968 : return assertInternalFact(atom, polarity, id, pfr, children, args);
56 : : }
57 : 14200 : return assertInternalFact(atom, polarity, id, reason);
58 : : }
59 : :
60 : 6796 : bool InferenceManager::arrayLemma(
61 : : Node conc, InferenceId id, Node exp, ProofRule pfr, LemmaProperty p)
62 : : {
63 [ + - ]: 13592 : Trace("arrays-infer") << "TheoryArrays::arrayLemma: " << conc << " by " << exp
64 : 6796 : << "; " << id << std::endl;
65 : 6796 : NodeManager* nm = nodeManager();
66 [ + + ]: 6796 : if (isProofEnabled())
67 : : {
68 : 3958 : std::vector<Node> children;
69 : 3958 : std::vector<Node> args;
70 : : // convert to proof rule application
71 : 1979 : convert(pfr, conc, exp, children, args);
72 : : // make the trusted lemma based on the eager proof generator and send
73 : 3958 : TrustNode tlem = d_lemmaPg->mkTrustNode(conc, pfr, children, args);
74 : 1979 : return trustedLemma(tlem, id, p);
75 : : }
76 : : // send lemma without proofs
77 : 9634 : Node lem = nm->mkNode(Kind::IMPLIES, exp, conc);
78 : 4817 : return lemma(lem, id, p);
79 : : }
80 : :
81 : 6947 : void InferenceManager::convert(ProofRule& id,
82 : : Node conc,
83 : : Node exp,
84 : : std::vector<Node>& children,
85 : : std::vector<Node>& args)
86 : : {
87 : : // note that children must contain something equivalent to exp,
88 : : // regardless of the ProofRule.
89 [ + + ][ + + ]: 6947 : switch (id)
[ + + ]
90 : : {
91 : 568 : case ProofRule::MACRO_SR_PRED_INTRO:
92 [ - + ][ - + ]: 568 : Assert(exp.isConst());
[ - - ]
93 : 568 : args.push_back(conc);
94 : 568 : break;
95 : 5195 : case ProofRule::ARRAYS_READ_OVER_WRITE:
96 [ + + ]: 5195 : if (exp.isConst())
97 : : {
98 : : // Premise can be shown by rewriting, use standard predicate intro rule.
99 : : // This is the case where we have 2 constant indices.
100 : 673 : id = ProofRule::MACRO_SR_PRED_INTRO;
101 : 673 : args.push_back(conc);
102 : : }
103 : : else
104 : : {
105 : 4522 : children.push_back(exp);
106 : 4522 : args.push_back(conc[0]);
107 : : }
108 : 5195 : break;
109 : 5 : case ProofRule::ARRAYS_READ_OVER_WRITE_CONTRA:
110 : 5 : children.push_back(exp);
111 : 5 : break;
112 : 662 : case ProofRule::ARRAYS_READ_OVER_WRITE_1:
113 [ - + ][ - + ]: 662 : Assert(exp.isConst());
[ - - ]
114 : 662 : args.push_back(conc[0]);
115 : 662 : break;
116 : 489 : case ProofRule::ARRAYS_EXT:
117 : : // since this rule depends on the ARRAY_DEQ_DIFF skolem which sorts
118 : : // indices, we assert that the equality is ordered here, which it should
119 : : // be based on the standard order for equality.
120 : 978 : Assert(exp.getKind() == Kind::NOT && exp[0].getKind() == Kind::EQUAL
121 : : && exp[0][0] < exp[0][1]);
122 : 489 : children.push_back(exp);
123 : 489 : break;
124 : 28 : default:
125 [ - + ]: 28 : if (id != ProofRule::TRUST)
126 : : {
127 : 0 : Assert(false) << "Unknown rule " << id << "\n";
128 : : }
129 : 28 : children.push_back(exp);
130 : 28 : args.push_back(mkTrustId(TrustId::THEORY_INFERENCE));
131 : 28 : args.push_back(conc);
132 : 28 : args.push_back(
133 : 56 : builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARRAYS));
134 : 28 : id = ProofRule::TRUST;
135 : 28 : break;
136 : : }
137 : 6947 : }
138 : :
139 : : } // namespace arrays
140 : : } // namespace theory
141 : : } // namespace cvc5::internal
|
