Skip to content

Commit 9053d18

Browse files
bpandreottibpandreotti
committed
Move premises outside Proof and into new Problem struct
1 parent f3f9107 commit 9053d18

File tree

16 files changed

+139
-126
lines changed

16 files changed

+139
-126
lines changed

‎carcara/src/ast/mod.rs

+2-15
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ mod node;
1010
mod polyeq;
1111
pub mod pool;
1212
pub(crate) mod printer;
13+
mod problem;
1314
mod proof;
1415
mod rc;
1516
mod substitution;
@@ -23,25 +24,11 @@ pub use node::{ProofNode, StepNode, SubproofNode};
2324
pub use polyeq::{alpha_equiv, polyeq, Polyeq, PolyeqComparable, PolyeqConfig};
2425
pub use pool::{PrimitivePool, TermPool};
2526
pub use printer::{print_proof, USE_SHARING_IN_TERM_DISPLAY};
27+
pub use problem::*;
2628
pub use proof::*;
2729
pub use rc::Rc;
2830
pub use substitution::{Substitution, SubstitutionError};
2931
pub use term::{Binder, BindingList, Constant, Operator, ParamOperator, Sort, SortedVar, Term};
3032

3133
#[cfg(test)]
3234
pub(crate) use node::compare_nodes;
33-
34-
/// The prelude of an SMT-LIB problem instance.
35-
///
36-
/// This stores the sort declarations, function declarations and the problem's logic string.
37-
#[derive(Debug, Clone, Default)]
38-
pub struct ProblemPrelude {
39-
/// The sort declarations, each represented by its name and arity.
40-
pub(crate) sort_declarations: Vec<(String, usize)>,
41-
42-
/// The function declarations, each represented by its name and body.
43-
pub(crate) function_declarations: Vec<(String, Rc<Term>)>,
44-
45-
/// The problem's logic string, if it exists.
46-
pub(crate) logic: Option<String>,
47-
}

‎carcara/src/ast/printer.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -613,11 +613,11 @@ mod tests {
613613
(step t6.t1 (cl (= (+ x 2) (+ x 2))) :rule hole)\n\
614614
(step t6 (cl) :rule hole)\n\
615615
";
616-
let (prelude, proof, mut pool) =
616+
let (problem, proof, mut pool) =
617617
parser::parse_instance(definitions, proof, parser::Config::new()).unwrap();
618618

619619
let mut buf = Vec::new();
620-
AlethePrinter::new(&mut pool, &prelude, true, &mut buf)
620+
AlethePrinter::new(&mut pool, &problem.prelude, true, &mut buf)
621621
.write_proof(&proof)
622622
.unwrap();
623623

‎carcara/src/ast/problem.rs

+41
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
use super::{Rc, Term};
2+
use indexmap::IndexSet;
3+
4+
/// An SMT problem in the SMT-LIB format.
5+
#[derive(Debug, Clone, Default)]
6+
pub struct Problem {
7+
/// The problem's prelude.
8+
pub prelude: ProblemPrelude,
9+
10+
/// The proof's premises.
11+
///
12+
/// Those are the terms introduced in the original problem's `assert` commands.
13+
pub premises: IndexSet<Rc<Term>>,
14+
}
15+
16+
impl Problem {
17+
pub fn new() -> Self {
18+
Self::default()
19+
}
20+
}
21+
22+
/// The prelude of an SMT-LIB problem instance.
23+
///
24+
/// This stores the sort declarations, function declarations and the problem's logic string.
25+
#[derive(Debug, Clone, Default)]
26+
pub struct ProblemPrelude {
27+
/// The sort declarations, each represented by its name and arity.
28+
pub(crate) sort_declarations: Vec<(String, usize)>,
29+
30+
/// The function declarations, each represented by its name and body.
31+
pub(crate) function_declarations: Vec<(String, Rc<Term>)>,
32+
33+
/// The problem's logic string, if it exists.
34+
pub(crate) logic: Option<String>,
35+
}
36+
37+
impl ProblemPrelude {
38+
pub fn new() -> Self {
39+
Self::default()
40+
}
41+
}

‎carcara/src/ast/proof.rs

-6
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,9 @@
11
use super::{ProofIter, Rc, SortedVar, Term};
22
use crate::CheckerError;
3-
use indexmap::IndexSet;
43

54
/// A proof in the Alethe format.
65
#[derive(Debug, Clone)]
76
pub struct Proof {
8-
/// The proof's premises.
9-
///
10-
/// Those are the terms introduced in the original problem's `assert` commands.
11-
pub premises: IndexSet<Rc<Term>>,
12-
137
/// The constants defined in the proof using `define-fun` with arity zero.
148
///
159
/// This is only used to reconstruct these `define-fun`s when printing the proof.

‎carcara/src/checker/mod.rs

+6-3
Original file line numberDiff line numberDiff line change
@@ -95,23 +95,26 @@ impl<'c> ProofChecker<'c> {
9595
}
9696
}
9797

98-
pub fn check(&mut self, proof: &Proof) -> CarcaraResult<bool> {
98+
pub fn check(&mut self, problem: &Problem, proof: &Proof) -> CarcaraResult<bool> {
9999
self.check_impl(
100+
problem,
100101
proof,
101102
None::<&mut CheckerStatistics<OnlineBenchmarkResults>>,
102103
)
103104
}
104105

105106
pub fn check_with_stats<CR: CollectResults + Send + Default>(
106107
&mut self,
108+
problem: &Problem,
107109
proof: &Proof,
108110
stats: &mut CheckerStatistics<CR>,
109111
) -> CarcaraResult<bool> {
110-
self.check_impl(proof, Some(stats))
112+
self.check_impl(problem, proof, Some(stats))
111113
}
112114

113115
fn check_impl<CR: CollectResults + Send + Default>(
114116
&mut self,
117+
problem: &Problem,
115118
proof: &Proof,
116119
mut stats: Option<&mut CheckerStatistics<CR>>,
117120
) -> CarcaraResult<bool> {
@@ -172,7 +175,7 @@ impl<'c> ProofChecker<'c> {
172175
}
173176
}
174177
ProofCommand::Assume { id, term } => {
175-
if !self.check_assume(id, term, &proof.premises, &iter, &mut stats) {
178+
if !self.check_assume(id, term, &problem.premises, &iter, &mut stats) {
176179
return Err(Error::Checker {
177180
inner: CheckerError::Assume(term.clone()),
178181
rule: "assume".into(),

‎carcara/src/checker/parallel/mod.rs

+11-2
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,12 @@ impl<'c> ParallelProofChecker<'c> {
6262
}
6363
}
6464

65-
pub fn check(&mut self, proof: &Proof, scheduler: &Scheduler) -> CarcaraResult<bool> {
65+
pub fn check(
66+
&mut self,
67+
problem: &Problem,
68+
proof: &Proof,
69+
scheduler: &Scheduler,
70+
) -> CarcaraResult<bool> {
6671
// Used to estimulate threads to abort prematurely (only happens when a
6772
// thread already found out an invalid step)
6873
let premature_abort = Arc::new(AtomicBool::new(false));
@@ -84,6 +89,7 @@ impl<'c> ParallelProofChecker<'c> {
8489
.stack_size(self.stack_size)
8590
.spawn_scoped(s, move || -> CarcaraResult<(bool, bool)> {
8691
local_self.worker_thread_check(
92+
problem,
8793
proof,
8894
schedule,
8995
local_pool,
@@ -130,6 +136,7 @@ impl<'c> ParallelProofChecker<'c> {
130136

131137
pub fn check_with_stats<CR: CollectResults + Send + Default>(
132138
&mut self,
139+
problem: &Problem,
133140
proof: &Proof,
134141
scheduler: &Scheduler,
135142
stats: &mut CheckerStatistics<CR>,
@@ -165,6 +172,7 @@ impl<'c> ParallelProofChecker<'c> {
165172
move || -> CarcaraResult<(bool, bool, CheckerStatistics<CR>)> {
166173
local_self
167174
.worker_thread_check(
175+
problem,
168176
proof,
169177
schedule,
170178
local_pool,
@@ -226,6 +234,7 @@ impl<'c> ParallelProofChecker<'c> {
226234

227235
fn worker_thread_check<CR: CollectResults + Send + Default>(
228236
&mut self,
237+
problem: &Problem,
229238
proof: &Proof,
230239
schedule: &Schedule,
231240
mut pool: LocalPool,
@@ -303,7 +312,7 @@ impl<'c> ParallelProofChecker<'c> {
303312
}
304313
}
305314
ProofCommand::Assume { id, term } => {
306-
if !self.check_assume(id, term, &proof.premises, &iter, &mut stats) {
315+
if !self.check_assume(id, term, &problem.premises, &iter, &mut stats) {
307316
// Signalize to other threads to stop the proof checking
308317
should_abort.store(true, Ordering::Release);
309318
return Err(Error::Checker {

‎carcara/src/checker/rules/mod.rs

+3-3
Original file line numberDiff line numberDiff line change
@@ -162,7 +162,7 @@ fn run_tests(test_name: &str, definitions: &str, cases: &[(&str, bool)]) {
162162

163163
for (i, (proof, expected)) in cases.iter().enumerate() {
164164
// This parses the definitions again for every case, which is not ideal
165-
let (_, mut proof, mut pool) = parser::parse_instance(
165+
let (mut problem, mut proof, mut pool) = parser::parse_instance(
166166
Cursor::new(definitions),
167167
Cursor::new(proof),
168168
parser::Config::new(),
@@ -172,7 +172,7 @@ fn run_tests(test_name: &str, definitions: &str, cases: &[(&str, bool)]) {
172172
// Since rule tests often use `assume` commands to introduce premises, we search the proof
173173
// for all `assume`d terms and retroactively add them as the problem premises, to avoid
174174
// checker errors on the `assume`s
175-
proof.premises = proof
175+
problem.premises = proof
176176
.commands
177177
.iter()
178178
.filter_map(|c| match c {
@@ -193,7 +193,7 @@ fn run_tests(test_name: &str, definitions: &str, cases: &[(&str, bool)]) {
193193
}));
194194

195195
let mut checker = checker::ProofChecker::new(&mut pool, checker::Config::new());
196-
let got = checker.check(&proof).is_ok();
196+
let got = checker.check(&problem, &proof).is_ok();
197197
assert_eq!(
198198
*expected, got,
199199
"test case \"{}\" index {} failed",

‎carcara/src/elaborator/hole.rs

+7-10
Original file line numberDiff line numberDiff line change
@@ -59,14 +59,14 @@ fn get_problem_string(
5959
}
6060

6161
pub fn hole(elaborator: &mut Elaborator, step: &StepNode) -> Option<Rc<ProofNode>> {
62-
let prelude = if elaborator.prelude.logic.clone().unwrap() == "QF_LIA" {
62+
let prelude = elaborator.problem.prelude.clone();
63+
let prelude = if prelude.logic.as_deref() == Some("QF_LIA") {
6364
ProblemPrelude {
64-
sort_declarations: elaborator.prelude.sort_declarations.clone(),
65-
function_declarations: elaborator.prelude.function_declarations.clone(),
6665
logic: Some("QF_LIRA".into()),
66+
..prelude
6767
}
6868
} else {
69-
elaborator.prelude.clone()
69+
prelude
7070
};
7171
let problem = get_problem_string(elaborator.pool, &prelude, &step.clause);
7272
let options = elaborator.config.hole_options.as_ref().unwrap();
@@ -150,14 +150,11 @@ fn parse_and_check_solver_proof(
150150
allow_int_real_subtyping: true,
151151
strict: false,
152152
};
153-
let mut parser = parser::Parser::new(pool, config, problem)?;
154-
let (_, premises) = parser.parse_problem()?;
155-
parser.reset(proof)?;
156-
let mut proof = parser.parse_proof()?;
157-
proof.premises = premises;
153+
154+
let (problem, proof) = parser::parse_instance_with_pool(problem, proof, config, pool)?;
158155

159156
let config = checker::Config::new();
160-
let res = checker::ProofChecker::new(pool, config).check(&proof)?;
157+
let res = checker::ProofChecker::new(pool, config).check(&problem, &proof)?;
161158
Ok((proof.commands, res))
162159
}
163160

‎carcara/src/elaborator/lia_generic.rs

+3-7
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ fn get_problem_string(
5959
}
6060

6161
pub fn lia_generic(elaborator: &mut Elaborator, step: &StepNode) -> Option<Rc<ProofNode>> {
62-
let problem = get_problem_string(elaborator.pool, elaborator.prelude, &step.clause);
62+
let problem = get_problem_string(elaborator.pool, &elaborator.problem.prelude, &step.clause);
6363
let options = elaborator.config.lia_options.as_ref().unwrap();
6464
let commands = match get_solver_proof(elaborator.pool, problem, options) {
6565
Ok(c) => c,
@@ -137,14 +137,10 @@ fn parse_and_check_solver_proof(
137137
allow_int_real_subtyping: true,
138138
strict: false,
139139
};
140-
let mut parser = parser::Parser::new(pool, config, problem)?;
141-
let (_, premises) = parser.parse_problem()?;
142-
parser.reset(proof)?;
143-
let mut proof = parser.parse_proof()?;
144-
proof.premises = premises;
140+
let (problem, proof) = parser::parse_instance_with_pool(problem, proof, config, pool)?;
145141

146142
let config = checker::Config::new().ignore_unknown_rules(true);
147-
checker::ProofChecker::new(pool, config).check(&proof)?;
143+
checker::ProofChecker::new(pool, config).check(&problem, &proof)?;
148144
Ok(proof.commands)
149145
}
150146

‎carcara/src/elaborator/mod.rs

+5-11
Original file line numberDiff line numberDiff line change
@@ -64,19 +64,13 @@ pub struct HoleOptions {
6464

6565
pub struct Elaborator<'e> {
6666
pool: &'e mut PrimitivePool,
67-
premises: &'e IndexSet<Rc<Term>>,
68-
prelude: &'e ProblemPrelude,
67+
problem: &'e Problem,
6968
config: Config,
7069
}
7170

7271
impl<'e> Elaborator<'e> {
73-
pub fn new(
74-
pool: &'e mut PrimitivePool,
75-
premises: &'e IndexSet<Rc<Term>>,
76-
prelude: &'e ProblemPrelude,
77-
config: Config,
78-
) -> Self {
79-
Self { pool, premises, prelude, config }
72+
pub fn new(pool: &'e mut PrimitivePool, problem: &'e Problem, config: Config) -> Self {
73+
Self { pool, problem, config }
8074
}
8175

8276
pub fn elaborate_with_default_pipeline(&mut self, root: &Rc<ProofNode>) -> Rc<ProofNode> {
@@ -148,7 +142,7 @@ impl<'e> Elaborator<'e> {
148142
mutate(root, |context, node| {
149143
match node.as_ref() {
150144
ProofNode::Assume { id, depth, term }
151-
if context.is_empty() && !self.premises.contains(term) =>
145+
if context.is_empty() && !self.problem.premises.contains(term) =>
152146
{
153147
self.elaborate_assume(id, *depth, term)
154148
}
@@ -186,7 +180,7 @@ impl<'e> Elaborator<'e> {
186180

187181
fn elaborate_assume(&mut self, id: &str, depth: usize, term: &Rc<Term>) -> Rc<ProofNode> {
188182
let mut found = None;
189-
for p in self.premises {
183+
for p in &self.problem.premises {
190184
if Polyeq::new()
191185
.mod_reordering(true)
192186
.mod_nary(true)

0 commit comments

Comments
 (0)