Skip to content

Commit

Permalink
Allow user to choose solver binary for lia_generic
Browse files Browse the repository at this point in the history
  • Loading branch information
bpandreotti committed Aug 8, 2023
1 parent 53e2576 commit bd2d55a
Show file tree
Hide file tree
Showing 8 changed files with 85 additions and 56 deletions.
28 changes: 14 additions & 14 deletions carcara/src/checker/error.rs
Original file line number Diff line number Diff line change
Expand Up @@ -248,29 +248,29 @@ pub enum LinearArithmeticError {

#[derive(Debug, Error)]
pub enum LiaGenericError {
#[error("failed to spawn cvc5 process")]
FailedSpawnCvc5(io::Error),
#[error("failed to spawn solver process")]
FailedSpawnSolver(io::Error),

#[error("failed to write to cvc5 stdin")]
FailedWriteToCvc5Stdin(io::Error),
#[error("failed to write to solver stdin")]
FailedWriteToSolverStdin(io::Error),

#[error("error while waiting for cvc5 to exit")]
FailedWaitForCvc5(io::Error),
#[error("error while waiting for solver to exit")]
FailedWaitForSolver(io::Error),

#[error("cvc5 gave invalid output")]
Cvc5GaveInvalidOutput,
#[error("solver gave invalid output")]
SolverGaveInvalidOutput,

#[error("cvc5 output not unsat")]
Cvc5OutputNotUnsat,
#[error("solver output not unsat")]
OutputNotUnsat,

#[error("cvc5 timed out when solving problem")]
Cvc5Timeout,
#[error("solver timed out when solving problem")]
SolverTimeout,

#[error(
"cvc5 returned non-zero exit code: {}",
"solver returned non-zero exit code: {}",
if let Some(i) = .0 { format!("{}", i) } else { "none".to_owned() }
)]
Cvc5NonZeroExitCode(Option<i32>),
NonZeroExitCode(Option<i32>),

#[error("error in inner proof: {0}")]
InnerProofError(Box<crate::Error>),
Expand Down
53 changes: 30 additions & 23 deletions carcara/src/checker/lia_generic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30,12 +30,13 @@ pub fn lia_generic_single_thread(
prelude: &ProblemPrelude,
elaborator: Option<&mut Elaborator>,
root_id: &str,
solver: &str,
) -> bool {
let problem = get_problem_string(conclusion, prelude);
let commands = match get_cvc5_proof(pool, problem) {
let commands = match get_solver_proof(pool, problem, solver) {
Ok(c) => c,
Err(e) => {
log::warn!("failed to check `lia_generic` step using cvc5: {}", e);
log::warn!("failed to check `lia_generic` step: {}", e);
if let Some(elaborator) = elaborator {
elaborator.unchanged(conclusion);
}
Expand All @@ -44,27 +45,32 @@ pub fn lia_generic_single_thread(
};

if let Some(elaborator) = elaborator {
insert_cvc5_proof(pool, elaborator, commands, conclusion, root_id);
insert_solver_proof(pool, elaborator, commands, conclusion, root_id);
}
false
}

pub fn lia_generic_multi_thread(conclusion: &[Rc<Term>], prelude: &ProblemPrelude) -> bool {
pub fn lia_generic_multi_thread(
conclusion: &[Rc<Term>],
prelude: &ProblemPrelude,
solver: &str,
) -> bool {
let mut pool = PrimitivePool::new();
let problem = get_problem_string(conclusion, prelude);
if let Err(e) = get_cvc5_proof(&mut pool, problem) {
log::warn!("failed to check `lia_generic` step using cvc5: {}", e);
if let Err(e) = get_solver_proof(&mut pool, problem, solver) {
log::warn!("failed to check `lia_generic` step using: {}", e);
true
} else {
false
}
}

fn get_cvc5_proof(
fn get_solver_proof(
pool: &mut PrimitivePool,
problem: String,
solver: &str,
) -> Result<Vec<ProofCommand>, LiaGenericError> {
let mut cvc5 = Command::new("cvc5")
let mut process = Command::new(solver)
.args([
"--tlimit=10000",
"--lang=smt2",
Expand All @@ -76,43 +82,44 @@ fn get_cvc5_proof(
.stdout(Stdio::piped())
.stderr(Stdio::piped())
.spawn()
.map_err(LiaGenericError::FailedSpawnCvc5)?;
.map_err(LiaGenericError::FailedSpawnSolver)?;

cvc5.stdin
process
.stdin
.take()
.expect("failed to open cvc5 stdin")
.expect("failed to open solver stdin")
.write_all(problem.as_bytes())
.map_err(LiaGenericError::FailedWriteToCvc5Stdin)?;
.map_err(LiaGenericError::FailedWriteToSolverStdin)?;

let output = cvc5
let output = process
.wait_with_output()
.map_err(LiaGenericError::FailedWaitForCvc5)?;
.map_err(LiaGenericError::FailedWaitForSolver)?;

if !output.status.success() {
if let Ok(s) = std::str::from_utf8(&output.stderr) {
if s.contains("cvc5 interrupted by timeout.") {
return Err(LiaGenericError::Cvc5Timeout);
if s.contains("interrupted by timeout.") {
return Err(LiaGenericError::SolverTimeout);
}
}
return Err(LiaGenericError::Cvc5NonZeroExitCode(output.status.code()));
return Err(LiaGenericError::NonZeroExitCode(output.status.code()));
}

let mut proof = output.stdout.as_slice();
let mut first_line = String::new();

proof
.read_line(&mut first_line)
.map_err(|_| LiaGenericError::Cvc5GaveInvalidOutput)?;
.map_err(|_| LiaGenericError::SolverGaveInvalidOutput)?;

if first_line.trim_end() != "unsat" {
return Err(LiaGenericError::Cvc5OutputNotUnsat);
return Err(LiaGenericError::OutputNotUnsat);
}

parse_and_check_cvc5_proof(pool, problem.as_bytes(), proof)
parse_and_check_solver_proof(pool, problem.as_bytes(), proof)
.map_err(|e| LiaGenericError::InnerProofError(Box::new(e)))
}

fn parse_and_check_cvc5_proof(
fn parse_and_check_solver_proof(
pool: &mut PrimitivePool,
problem: &[u8],
proof: &[u8],
Expand Down Expand Up @@ -190,7 +197,7 @@ fn insert_missing_assumes(
(all, num_added)
}

fn insert_cvc5_proof(
fn insert_solver_proof(
pool: &mut PrimitivePool,
elaborator: &mut Elaborator,
mut commands: Vec<ProofCommand>,
Expand All @@ -206,7 +213,7 @@ fn insert_cvc5_proof(
conclusion,
&commands,
// This is a bit ugly, but we have to add the ".added" to avoid colliding with the first few
// steps in the cvc5 proof
// steps in the solver proof
&format!("{}.added", root_id),
);

Expand Down
9 changes: 5 additions & 4 deletions carcara/src/checker/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ pub struct Config {
strict: bool,
skip_unknown_rules: bool,
is_running_test: bool,
lia_via_cvc5: bool,
lia_solver: Option<Box<str>>,
}

impl Config {
Expand All @@ -68,8 +68,8 @@ impl Config {
self
}

pub fn lia_via_cvc5(mut self, value: bool) -> Self {
self.lia_via_cvc5 = value;
pub fn lia_solver(mut self, value: impl Into<Option<Box<str>>>) -> Self {
self.lia_solver = value.into();
self
}
}
Expand Down Expand Up @@ -340,13 +340,14 @@ impl<'c> ProofChecker<'c> {

let mut elaborated = false;
if step.rule == "lia_generic" {
if self.config.lia_via_cvc5 {
if let Some(solver) = &self.config.lia_solver {
let is_hole = lia_generic::lia_generic_single_thread(
self.pool,
&step.clause,
self.prelude,
self.elaborator.as_mut(),
&step.id,
solver,
);
self.is_holey = self.is_holey || is_hole;
elaborated = self.elaborator.is_some();
Expand Down
5 changes: 3 additions & 2 deletions carcara/src/checker/parallel/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -422,8 +422,9 @@ impl<'c> ParallelProofChecker<'c> {
let mut polyeq_time = Duration::ZERO;

if step.rule == "lia_generic" {
if self.config.lia_via_cvc5 {
let is_hole = lia_generic::lia_generic_multi_thread(&step.clause, self.prelude);
if let Some(solver) = &self.config.lia_solver {
let is_hole =
lia_generic::lia_generic_multi_thread(&step.clause, self.prelude, solver);
self.is_holey = self.is_holey || is_hole;
} else {
log::warn!("encountered \"lia_generic\" rule, ignoring");
Expand Down
2 changes: 1 addition & 1 deletion carcara/src/checker/rules/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -173,7 +173,7 @@ fn run_tests(test_name: &str, definitions: &str, cases: &[(&str, bool)]) {
strict: false,
skip_unknown_rules: false,
is_running_test: true,
lia_via_cvc5: false,
lia_solver: None,
},
&prelude,
);
Expand Down
17 changes: 9 additions & 8 deletions carcara/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -72,11 +72,12 @@ pub struct CarcaraOptions {
/// to a function that expects a `Real` will still be an error.
pub allow_int_real_subtyping: bool,

/// Enable checking/elaboration of `lia_generic` steps using cvc5. When checking a proof, this
/// will call cvc5 to solve the linear integer arithmetic problem, check the proof, and discard
/// it. When elaborating, the proof will instead be inserted in the place of the `lia_generic`
/// step.
pub lia_via_cvc5: bool,
/// Enable checking/elaboration of `lia_generic` steps using the given solver. When checking a
/// proof, this will call the solver to solve the linear integer arithmetic problem, check the
/// proof, and discard it. When elaborating, the proof will instead be inserted in the place of
/// the `lia_generic` step. The solver should be a binary that can read SMT-LIB from stdin and
/// output an Alethe proof from stdout.
pub lia_solver: Option<Box<str>>,

/// Enables "strict" checking of some rules.
///
Expand Down Expand Up @@ -152,7 +153,7 @@ pub fn check<T: io::BufRead>(problem: T, proof: T, options: CarcaraOptions) -> R
let config = checker::Config::new()
.strict(options.strict)
.skip_unknown_rules(options.skip_unknown_rules)
.lia_via_cvc5(options.lia_via_cvc5);
.lia_solver(options.lia_solver);

// Checking
let checking = Instant::now();
Expand Down Expand Up @@ -218,7 +219,7 @@ pub fn check_parallel<T: io::BufRead>(
let config = checker::Config::new()
.strict(options.strict)
.skip_unknown_rules(options.skip_unknown_rules)
.lia_via_cvc5(options.lia_via_cvc5);
.lia_solver(options.lia_solver);

// Checking
let checking = Instant::now();
Expand Down Expand Up @@ -289,7 +290,7 @@ pub fn check_and_elaborate<T: io::BufRead>(
let config = checker::Config::new()
.strict(options.strict)
.skip_unknown_rules(options.skip_unknown_rules)
.lia_via_cvc5(options.lia_via_cvc5);
.lia_solver(options.lia_solver);

// Checking
let checking = Instant::now();
Expand Down
2 changes: 1 addition & 1 deletion cli/src/benchmarking.rs
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ fn run_job<T: CollectResults + Default + Send>(
let config = checker::Config::new()
.strict(options.strict)
.skip_unknown_rules(options.skip_unknown_rules)
.lia_via_cvc5(options.lia_via_cvc5);
.lia_solver(options.lia_solver.clone());
let mut checker = checker::ProofChecker::new(&mut pool, config, &prelude);

let checking = Instant::now();
Expand Down
25 changes: 22 additions & 3 deletions cli/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ struct ParsingOptions {
allow_int_real_subtyping: bool,
}

#[derive(Args, Clone, Copy)]
#[derive(Args, Clone)]
struct CheckingOptions {
/// Enables the strict checking of certain rules.
#[clap(short, long)]
Expand All @@ -127,8 +127,12 @@ struct CheckingOptions {
#[clap(long)]
skip_unknown_rules: bool,

/// Check `lia_generic` steps by calling into cvc5.
/// Check `lia_generic` steps using the provided solver.
#[clap(long)]
lia_solver: Option<String>,

/// Check `lia_generic` steps by calling into cvc5 (deprecated).
#[clap(long, conflicts_with("lia-solver"))]
lia_via_cvc5: bool,
}

Expand All @@ -148,15 +152,21 @@ fn build_carcara_options(
CheckingOptions {
strict,
skip_unknown_rules,
lia_solver,
lia_via_cvc5,
}: CheckingOptions,
StatsOptions { stats }: StatsOptions,
) -> CarcaraOptions {
// If no solver is provided by the `--lia-solver` option, *and* the `--lia-via-cvc5` option was
// passed, we default to cvc5 as a solver
let lia_solver = lia_solver
.map(Into::into)
.or_else(|| lia_via_cvc5.then(|| "cvc5".into()));
CarcaraOptions {
apply_function_defs,
expand_lets: expand_let_bindings,
allow_int_real_subtyping,
lia_via_cvc5,
lia_solver,
strict,
skip_unknown_rules,
stats,
Expand Down Expand Up @@ -301,6 +311,15 @@ fn main() {
let colors_enabled = !cli.no_color && atty::is(atty::Stream::Stderr);
logger::init(cli.log_level.into(), colors_enabled);

if let Command::Check(CheckCommandOptions { checking, .. })
| Command::Elaborate(ElaborateCommandOptions { checking, .. })
| Command::Bench(BenchCommandOptions { checking, .. }) = &cli.command
{
if checking.lia_via_cvc5 {
log::warn!("`--lia-via-cvc5` option is deprecated, please use `--lia-solver cvc5`")
}
}

let result = match cli.command {
Command::Parse(options) => parse_command(options),
Command::Check(options) => {
Expand Down

0 comments on commit bd2d55a

Please sign in to comment.