Skip to content

Commit 189a5dd

Browse files
ajreynolajreynol
authored
Add lemma inprocessing technique (cvc5#10319)
This can be used to minimize the number of new SAT literals introduced in quantifier instantiations. It has a positive overall impact on SMT-LIB quantifiers, but is disabled by default for now.
1 parent 3d86669 commit 189a5dd

18 files changed

+475
-20
lines changed

‎src/CMakeLists.txt

+2
Original file line numberDiff line numberDiff line change
@@ -246,6 +246,8 @@ libcvc5_add_sources(
246246
prop/kissat.h
247247
prop/learned_db.cpp
248248
prop/learned_db.h
249+
prop/lemma_inprocess.cpp
250+
prop/lemma_inprocess.h
249251
prop/minisat/core/Dimacs.h
250252
prop/minisat/core/Solver.cc
251253
prop/minisat/core/Solver.h

‎src/options/theory_options.toml

+41
Original file line numberDiff line numberDiff line change
@@ -66,3 +66,44 @@ name = "Theory Layer"
6666
[[option.mode.CARE_GRAPH]]
6767
name = "care-graph"
6868
help = "Use care graphs for theory combination."
69+
70+
[[option]]
71+
name = "lemmaInprocess"
72+
category = "expert"
73+
long = "lemma-inprocess=MODE"
74+
type = "LemmaInprocessMode"
75+
default = "NONE"
76+
help = "Modes for inprocessing lemmas."
77+
help_mode = "Modes for inprocessing lemmas."
78+
[[option.mode.FULL]]
79+
name = "full"
80+
help = "Full inprocessing."
81+
[[option.mode.LIGHT]]
82+
name = "light"
83+
help = "Light inprocessing."
84+
[[option.mode.NONE]]
85+
name = "none"
86+
help = "No inprocessing."
87+
88+
[[option]]
89+
name = "lemmaInprocessSubsMode"
90+
category = "expert"
91+
long = "lemma-inprocess-subs=MODE"
92+
type = "LemmaInprocessSubsMode"
93+
default = "SIMPLE"
94+
help = "Modes for substitutions for inprocessing lemmas."
95+
help_mode = "Modes for substitutions for inprocessing lemmas."
96+
[[option.mode.ALL]]
97+
name = "all"
98+
help = "All substitutions."
99+
[[option.mode.SIMPLE]]
100+
name = "simple"
101+
help = "Simple substitutions."
102+
103+
[[option]]
104+
name = "lemmaInprocessInferEqLit"
105+
category = "expert"
106+
long = "lemma-inprocess-infer-eq-lit"
107+
type = "bool"
108+
default = "false"
109+
help = "Infer equivalent literals when using lemma inprocess"

‎src/proof/trust_node.cpp

+5
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,11 @@ TrustNode TrustNode::mkReplaceGenTrustNode(const TrustNode& orig,
7474
return TrustNode(orig.getKind(), orig.getProven(), g);
7575
}
7676

77+
TrustNode TrustNode::mkTrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g)
78+
{
79+
return TrustNode(tnk, p, g);
80+
}
81+
7782
TrustNode TrustNode::null()
7883
{
7984
return TrustNode(TrustNodeKind::INVALID, Node::null());

‎src/proof/trust_node.h

+4
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,10 @@ class TrustNode
9696
/** Make a trust node, replacing the original generator */
9797
static TrustNode mkReplaceGenTrustNode(const TrustNode& orig,
9898
ProofGenerator* g);
99+
/** Make a trust node with the given explicit arguments. */
100+
static TrustNode mkTrustNode(TrustNodeKind tnk,
101+
Node p,
102+
ProofGenerator* g = nullptr);
99103
/** The null proven node */
100104
static TrustNode null();
101105
~TrustNode() {}

‎src/prop/lemma_inprocess.cpp

+175
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,175 @@
1+
/******************************************************************************
2+
* Top contributors (to current version):
3+
* Andrew Reynolds
4+
*
5+
* This file is part of the cvc5 project.
6+
*
7+
* Copyright (c) 2009-2023 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+
* Learner for literals asserted at level zero.
14+
*/
15+
16+
#include "prop/lemma_inprocess.h"
17+
18+
#include "expr/node_algorithm.h"
19+
#include "options/theory_options.h"
20+
#include "prop/zero_level_learner.h"
21+
#include "smt/env.h"
22+
23+
namespace cvc5::internal {
24+
namespace prop {
25+
26+
LemmaInprocess::LemmaInprocess(Env& env, CnfStream* cs, ZeroLevelLearner& zll)
27+
: EnvObj(env),
28+
d_cs(cs),
29+
d_tsmap(zll.getSimplifications()),
30+
d_subsLitMap(userContext()),
31+
d_eqLitLemmas(userContext())
32+
{
33+
}
34+
TrustNode LemmaInprocess::inprocessLemma(TrustNode& trn)
35+
{
36+
if (trn.getKind() == TrustNodeKind::CONFLICT)
37+
{
38+
return trn;
39+
}
40+
const Node& proven = trn.getProven();
41+
Node provenp = processInternal(proven);
42+
if (provenp != proven)
43+
{
44+
Trace("lemma-inprocess-lemma")
45+
<< "Inprocess " << proven << " returns " << provenp << std::endl;
46+
// proofs not supported
47+
return TrustNode::mkTrustNode(trn.getKind(), provenp);
48+
}
49+
return trn;
50+
}
51+
52+
Node LemmaInprocess::processInternal(const Node& lem)
53+
{
54+
std::vector<Node> eqLitLemmas;
55+
NodeManager* nm = NodeManager::currentNM();
56+
std::unordered_map<TNode, Node> visited;
57+
std::unordered_map<TNode, Node>::iterator it;
58+
std::vector<TNode> visit;
59+
context::CDHashMap<Node, Node>::iterator its;
60+
TNode cur;
61+
visit.emplace_back(lem);
62+
do
63+
{
64+
cur = visit.back();
65+
Trace("lemma-inprocess-visit") << "visit " << cur << std::endl;
66+
Assert(cur.getType().isBoolean());
67+
it = visited.find(cur);
68+
if (it == visited.end())
69+
{
70+
if (expr::isBooleanConnective(cur))
71+
{
72+
visited[cur] = Node::null();
73+
visit.insert(visit.end(), cur.begin(), cur.end());
74+
}
75+
else
76+
{
77+
visit.pop_back();
78+
// literal case
79+
bool prevLit = d_cs->hasLiteral(cur);
80+
Node scur = d_tsmap.get().apply(cur, d_env.getRewriter());
81+
its = d_subsLitMap.find(scur);
82+
if (its != d_subsLitMap.end())
83+
{
84+
if (cur != its->second)
85+
{
86+
Trace("lemma-inprocess")
87+
<< "Replace (indirect): " << cur << " -> " << its->second
88+
<< ", prevLit = " << prevLit << std::endl;
89+
visited[cur] = its->second;
90+
continue;
91+
}
92+
}
93+
else
94+
{
95+
bool currLit = prevLit;
96+
if (scur != cur)
97+
{
98+
currLit = d_cs->hasLiteral(scur);
99+
scur = rewrite(scur);
100+
Trace("lemma-inprocess-debug")
101+
<< "Inprocess " << cur << " -> " << scur << std::endl;
102+
bool doReplace = false;
103+
switch (options().theory.lemmaInprocess)
104+
{
105+
case options::LemmaInprocessMode::FULL:
106+
doReplace = (scur.isConst() || currLit || !prevLit);
107+
break;
108+
case options::LemmaInprocessMode::LIGHT:
109+
doReplace = (scur.isConst() || (currLit && !prevLit));
110+
break;
111+
default: break;
112+
}
113+
if (doReplace)
114+
{
115+
if (options().theory.lemmaInprocessInferEqLit
116+
&& ((scur.isConst() || currLit) && prevLit))
117+
{
118+
// inferred they are equivalent? maybe should send clause here?
119+
Node eql = rewrite(scur.eqNode(cur));
120+
if (d_eqLitLemmas.find(eql) == d_eqLitLemmas.end())
121+
{
122+
d_eqLitLemmas.insert(eql);
123+
eqLitLemmas.emplace_back(eql);
124+
}
125+
}
126+
Trace("lemma-inprocess")
127+
<< "Replace: " << cur << " -> " << scur
128+
<< ", currLit = " << currLit << ", prevLit = " << prevLit
129+
<< std::endl;
130+
visited[cur] = scur;
131+
d_subsLitMap[scur] = scur;
132+
continue;
133+
}
134+
}
135+
d_subsLitMap[scur] = cur;
136+
}
137+
visited[cur] = cur;
138+
}
139+
continue;
140+
}
141+
visit.pop_back();
142+
if (it->second.isNull())
143+
{
144+
Node ret = cur;
145+
bool childChanged = false;
146+
std::vector<Node> children;
147+
for (const Node& cn : cur)
148+
{
149+
it = visited.find(cn);
150+
Assert(it != visited.end());
151+
Assert(!it->second.isNull());
152+
childChanged = childChanged || cn != it->second;
153+
children.push_back(it->second);
154+
}
155+
if (childChanged)
156+
{
157+
ret = nm->mkNode(cur.getKind(), children);
158+
ret = rewrite(ret);
159+
}
160+
visited[cur] = ret;
161+
}
162+
} while (!visit.empty());
163+
Assert(visited.find(lem) != visited.end());
164+
Assert(!visited.find(lem)->second.isNull());
165+
Node ret = visited[lem];
166+
if (!eqLitLemmas.empty())
167+
{
168+
eqLitLemmas.emplace_back(ret);
169+
return nm->mkAnd(eqLitLemmas);
170+
}
171+
return ret;
172+
}
173+
174+
} // namespace prop
175+
} // namespace cvc5::internal

‎src/prop/lemma_inprocess.h

+86
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
/******************************************************************************
2+
* Top contributors (to current version):
3+
* Andrew Reynolds
4+
*
5+
* This file is part of the cvc5 project.
6+
*
7+
* Copyright (c) 2009-2023 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+
* Learner for literals asserted at level zero.
14+
*/
15+
16+
#include "cvc5_private.h"
17+
18+
#ifndef CVC5__PROP__LEMMA_INPROCESS_H
19+
#define CVC5__PROP__LEMMA_INPROCESS_H
20+
21+
#include <unordered_set>
22+
23+
#include "context/cdhashset.h"
24+
#include "context/cdo.h"
25+
#include "expr/node.h"
26+
#include "prop/cnf_stream.h"
27+
#include "smt/env_obj.h"
28+
#include "theory/trust_substitutions.h"
29+
30+
namespace cvc5::internal {
31+
32+
class TheoryEngine;
33+
34+
namespace prop {
35+
36+
class ZeroLevelLearner;
37+
38+
/**
39+
* Lemma inprocess, which heuristically simplifies lemmas to an equivalent
40+
* form based on the current simplifications stored by the zero level learner.
41+
*
42+
* The intution of this class is to increase the likelihood that literals in the
43+
* SAT solver are reused. For example if a = 0 is learned at decision level
44+
* zero, and there is a SAT literal P(0), if P(a) is introduced as a new literal
45+
* in a lemma, we may replace it by P(0).
46+
*
47+
* As another example, if we learn a=b, c=b and we have a literal P(a), then
48+
* we may replace P(c) with P(a).
49+
*
50+
* This simplification is done selectively and will never replace a known SAT
51+
* literal by a new SAT literal. Further policies are determined by
52+
* lemma-inprocess-mode.
53+
*
54+
* Generally this method can only be applied to lemmas where the structure of
55+
* the lemma is not important. This includes quantifier instantiation lemmas
56+
* for example.
57+
*/
58+
class LemmaInprocess : protected EnvObj
59+
{
60+
using NodeSet = context::CDHashSet<Node>;
61+
62+
public:
63+
LemmaInprocess(Env& env, CnfStream* cs, ZeroLevelLearner& zll);
64+
~LemmaInprocess() {}
65+
/** Inprocess lemma */
66+
TrustNode inprocessLemma(TrustNode& trn);
67+
68+
private:
69+
/**
70+
* Process internal, returns an equivalent formula to lem, assuming d_tsmap.
71+
*/
72+
Node processInternal(const Node& lem);
73+
/** Pointer to CNF stream */
74+
CnfStream* d_cs;
75+
/** Reference to the current available simplification */
76+
theory::TrustSubstitutionMap& d_tsmap;
77+
/** Mapping from simplified literals to a known SAT literal */
78+
context::CDHashMap<Node, Node> d_subsLitMap;
79+
/** Equivalent literal lemmas we have sent */
80+
context::CDHashSet<Node> d_eqLitLemmas;
81+
};
82+
83+
} // namespace prop
84+
} // namespace cvc5::internal
85+
86+
#endif

‎src/prop/prop_engine.cpp

+11-3
Original file line numberDiff line numberDiff line change
@@ -175,6 +175,7 @@ void PropEngine::assertInputFormulas(
175175
void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p)
176176
{
177177
bool removable = isLemmaPropertyRemovable(p);
178+
bool inprocess = isLemmaPropertyInprocess(p);
178179

179180
// call preprocessor
180181
std::vector<theory::SkolemLemma> ppLemmas;
@@ -208,7 +209,7 @@ void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p)
208209
}
209210

210211
// now, assert the lemmas
211-
assertLemmasInternal(tplemma, ppLemmas, removable);
212+
assertLemmasInternal(tplemma, ppLemmas, removable, inprocess);
212213
}
213214

214215
void PropEngine::assertTrustedLemmaInternal(TrustNode trn, bool removable)
@@ -274,7 +275,8 @@ void PropEngine::assertInternal(
274275
void PropEngine::assertLemmasInternal(
275276
TrustNode trn,
276277
const std::vector<theory::SkolemLemma>& ppLemmas,
277-
bool removable)
278+
bool removable,
279+
bool inprocess)
278280
{
279281
if (!removable)
280282
{
@@ -290,6 +292,12 @@ void PropEngine::assertLemmasInternal(
290292
Trace("prop") << "Push to SAT..." << std::endl;
291293
if (!trn.isNull())
292294
{
295+
// inprocess
296+
if (inprocess
297+
&& options().theory.lemmaInprocess != options::LemmaInprocessMode::NONE)
298+
{
299+
trn = d_theoryProxy->inprocessLemma(trn);
300+
}
293301
assertTrustedLemmaInternal(trn, removable);
294302
}
295303
for (const theory::SkolemLemma& lem : ppLemmas)
@@ -558,7 +566,7 @@ Node PropEngine::getPreprocessedTerm(TNode n)
558566
TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas);
559567
// send lemmas corresponding to the skolems introduced by preprocessing n
560568
TrustNode trnNull;
561-
assertLemmasInternal(trnNull, newLemmas, false);
569+
assertLemmasInternal(trnNull, newLemmas, false, false);
562570
return tpn.isNull() ? Node(n) : tpn.getNode();
563571
}
564572

‎src/prop/prop_engine.h

+2-1
Original file line numberDiff line numberDiff line change
@@ -397,7 +397,8 @@ class PropEngine : protected EnvObj
397397
*/
398398
void assertLemmasInternal(TrustNode trn,
399399
const std::vector<theory::SkolemLemma>& ppLemmas,
400-
bool removable);
400+
bool removable,
401+
bool inprocess);
401402

402403
/**
403404
* Indicates that the SAT solver is currently solving something and we should

0 commit comments

Comments
 (0)