implement problems around complete
This commit is contained in:
parent
7a3ed4a994
commit
9fafc537e6
|
@ -9,7 +9,7 @@ use crate::{
|
|||
Result,
|
||||
};
|
||||
|
||||
use super::{LoopControl, MultishotProblem, Problem, SolverState};
|
||||
use super::{LoopControl, MultishotProblem, Problem, SetTheory, SolverState};
|
||||
|
||||
/// Compute all admissible extensions for an [`Aba`]
|
||||
#[derive(Default, Debug)]
|
||||
|
@ -32,18 +32,10 @@ pub struct DecideCredulousAdmissibility<A> {
|
|||
pub assumption: A,
|
||||
}
|
||||
|
||||
/// *(Literal)* `A` is element of `th(S)`
|
||||
#[derive(Debug)]
|
||||
pub struct SetTheory<A: Atom>(A);
|
||||
|
||||
/// Helper for [`SetTheory`]
|
||||
#[derive(Debug)]
|
||||
pub struct SetTheoryHelper<A: Atom>(usize, A);
|
||||
|
||||
fn initial_clauses<A: Atom>(aba: &Aba<A>) -> ClauseList {
|
||||
pub fn initial_admissibility_clauses<I: TheoryAtom<A>, A: Atom>(aba: &Aba<A>) -> ClauseList {
|
||||
let mut clauses = vec![];
|
||||
// Create inference for the problem set
|
||||
theory_helper::<SetTheory<_>, _>(aba).collect_into(&mut clauses);
|
||||
theory_helper::<I, _>(aba).collect_into(&mut clauses);
|
||||
// Attack the inference of the aba, if an attack exists
|
||||
for (assumption, inverse) in &aba.inverses {
|
||||
[
|
||||
|
@ -99,7 +91,7 @@ impl<A: Atom> Problem<A> for SampleAdmissibleExtension {
|
|||
type Output = HashSet<A>;
|
||||
|
||||
fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList {
|
||||
let mut clauses = initial_clauses(aba);
|
||||
let mut clauses = initial_admissibility_clauses::<SetTheory<_>, _>(aba);
|
||||
// Prevent the empty set
|
||||
let no_empty_set: Clause = aba
|
||||
.inverses
|
||||
|
@ -125,7 +117,7 @@ impl<A: Atom> MultishotProblem<A> for EnumerateAdmissibleExtensions<A> {
|
|||
fn additional_clauses(&self, aba: &Aba<A>, iteration: usize) -> ClauseList {
|
||||
match iteration {
|
||||
0 => {
|
||||
let mut clauses = initial_clauses(aba);
|
||||
let mut clauses = initial_admissibility_clauses::<SetTheory<_>, _>(aba);
|
||||
// Prevent the empty set
|
||||
let no_empty_set: Clause = aba
|
||||
.inverses
|
||||
|
@ -193,7 +185,7 @@ impl<A: Atom> Problem<A> for VerifyAdmissibleExtension<A> {
|
|||
type Output = bool;
|
||||
|
||||
fn additional_clauses(&self, aba: &Aba<A>) -> crate::clauses::ClauseList {
|
||||
let mut clauses = initial_clauses(aba);
|
||||
let mut clauses = initial_admissibility_clauses::<SetTheory<_>, _>(aba);
|
||||
// Force inference on all members of the set
|
||||
for assumption in aba.assumptions() {
|
||||
let inf = SetTheory::new(assumption.clone());
|
||||
|
@ -229,7 +221,7 @@ impl<A: Atom> Problem<A> for DecideCredulousAdmissibility<A> {
|
|||
type Output = bool;
|
||||
|
||||
fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList {
|
||||
let mut clauses = initial_clauses(aba);
|
||||
let mut clauses = initial_admissibility_clauses::<SetTheory<_>, _>(aba);
|
||||
clauses.push(Clause::from(vec![SetTheory(self.assumption.clone()).pos()]));
|
||||
clauses
|
||||
}
|
||||
|
@ -249,15 +241,3 @@ impl<A: Atom> Problem<A> for DecideCredulousAdmissibility<A> {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<A: Atom> TheoryAtom<A> for SetTheory<A> {
|
||||
type Helper = SetTheoryHelper<A>;
|
||||
|
||||
fn new(atom: A) -> Self {
|
||||
Self(atom)
|
||||
}
|
||||
|
||||
fn new_helper(idx: usize, atom: A) -> Self::Helper {
|
||||
SetTheoryHelper(idx, atom)
|
||||
}
|
||||
}
|
||||
|
|
122
src/aba/problems/complete.rs
Normal file
122
src/aba/problems/complete.rs
Normal file
|
@ -0,0 +1,122 @@
|
|||
use std::collections::HashSet;
|
||||
|
||||
use crate::{
|
||||
aba::{Aba, Theory},
|
||||
clauses::{Atom, Clause, ClauseList},
|
||||
error::Error,
|
||||
literal::{IntoLiteral, TheoryAtom},
|
||||
Result,
|
||||
};
|
||||
|
||||
use super::{
|
||||
admissibility::initial_admissibility_clauses, LoopControl, MultishotProblem, Problem,
|
||||
SetTheory, SolverState,
|
||||
};
|
||||
|
||||
#[derive(Debug, Default)]
|
||||
pub struct EnumerateCompleteExtensions<A> {
|
||||
found: Vec<HashSet<A>>,
|
||||
}
|
||||
|
||||
/// Decide whether `assumption` is credulously complete in an [`Aba`]
|
||||
pub struct DecideCredulousComplete<A> {
|
||||
pub assumption: A,
|
||||
}
|
||||
|
||||
fn initial_complete_clauses<A: Atom>(aba: &Aba<A>) -> ClauseList {
|
||||
// Take everything from admissibility
|
||||
let mut clauses = initial_admissibility_clauses::<SetTheory<_>, _>(aba);
|
||||
// Additional complete logic
|
||||
for (assumption, inverse) in &aba.inverses {
|
||||
// For any assumption `a` and it's inverse `b`:
|
||||
// b not in th(A) => a in th(S)
|
||||
clauses.push(Clause::from(vec![
|
||||
Theory(inverse.clone()).pos(),
|
||||
SetTheory(assumption.clone()).pos(),
|
||||
]));
|
||||
}
|
||||
clauses
|
||||
}
|
||||
|
||||
impl<A: Atom> MultishotProblem<A> for EnumerateCompleteExtensions<A> {
|
||||
type Output = Vec<HashSet<A>>;
|
||||
|
||||
fn additional_clauses(&self, aba: &Aba<A>, iteration: usize) -> ClauseList {
|
||||
match iteration {
|
||||
0 => initial_complete_clauses(aba),
|
||||
idx => {
|
||||
// If we've found {a, c, d} in the last iteration, prevent it from being picked again
|
||||
// Assuming a..=f are our assumptions:
|
||||
// {-a, b, -c, -d, e, f} must be true
|
||||
let just_found = &self.found[idx - 1];
|
||||
let new_clause = aba
|
||||
.inverses
|
||||
.keys()
|
||||
.map(|assumption| {
|
||||
if just_found.contains(assumption) {
|
||||
SetTheory::new(assumption.clone()).neg()
|
||||
} else {
|
||||
SetTheory::new(assumption.clone()).pos()
|
||||
}
|
||||
})
|
||||
.collect();
|
||||
vec![new_clause]
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn feedback(&mut self, state: SolverState<'_, A>) -> LoopControl {
|
||||
if !state.sat_result {
|
||||
return LoopControl::Stop;
|
||||
}
|
||||
// TODO: Somehow query the mapper about things instead of this
|
||||
let found = state
|
||||
.aba
|
||||
.inverses
|
||||
.keys()
|
||||
.filter_map(|assumption| {
|
||||
let literal = SetTheory::new(assumption.clone()).pos();
|
||||
let raw = state.map.get_raw(&literal)?;
|
||||
match state.solver.value(raw) {
|
||||
Some(true) => Some(assumption.clone()),
|
||||
_ => None,
|
||||
}
|
||||
})
|
||||
.collect();
|
||||
self.found.push(found);
|
||||
LoopControl::Continue
|
||||
}
|
||||
|
||||
fn construct_output(
|
||||
self,
|
||||
_state: SolverState<'_, A>,
|
||||
_total_iterations: usize,
|
||||
) -> Self::Output {
|
||||
self.found
|
||||
}
|
||||
}
|
||||
|
||||
impl<A: Atom> Problem<A> for DecideCredulousComplete<A> {
|
||||
type Output = bool;
|
||||
|
||||
fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList {
|
||||
let mut clauses = initial_complete_clauses(aba);
|
||||
clauses.push(Clause::from(vec![SetTheory(self.assumption.clone()).pos()]));
|
||||
clauses
|
||||
}
|
||||
|
||||
fn construct_output(self, state: SolverState<'_, A>) -> Self::Output {
|
||||
state.sat_result
|
||||
}
|
||||
|
||||
fn check(&self, aba: &Aba<A>) -> Result {
|
||||
if aba.has_assumption(&self.assumption) {
|
||||
Ok(())
|
||||
} else {
|
||||
Err(Error::ProblemCheckFailed(format!(
|
||||
"Assumption {:?} not present in ABA framework",
|
||||
self.assumption
|
||||
)))
|
||||
}
|
||||
}
|
||||
}
|
|
@ -3,12 +3,14 @@ use cadical::Solver;
|
|||
use crate::{
|
||||
clauses::{Atom, ClauseList},
|
||||
error::{Error, Result},
|
||||
literal::TheoryAtom,
|
||||
mapper::Mapper,
|
||||
};
|
||||
|
||||
use super::Aba;
|
||||
|
||||
pub mod admissibility;
|
||||
pub mod complete;
|
||||
pub mod conflict_free;
|
||||
|
||||
#[derive(Debug, PartialEq, Eq, Clone, Copy)]
|
||||
|
@ -47,6 +49,14 @@ pub trait MultishotProblem<A: Atom> {
|
|||
}
|
||||
}
|
||||
|
||||
/// *(Literal)* `A` is element of `th(S)`
|
||||
#[derive(Debug)]
|
||||
pub struct SetTheory<A: Atom>(A);
|
||||
|
||||
/// Helper for [`SetTheory`]
|
||||
#[derive(Debug)]
|
||||
pub struct SetTheoryHelper<A: Atom>(usize, A);
|
||||
|
||||
pub fn solve<A: Atom, P: Problem<A>>(problem: P, aba: &Aba<A>) -> Result<P::Output> {
|
||||
problem.check(aba)?;
|
||||
let clauses = aba.derive_clauses();
|
||||
|
@ -111,3 +121,15 @@ pub fn multishot_solve<A: Atom, P: MultishotProblem<A>>(
|
|||
iteration,
|
||||
))
|
||||
}
|
||||
|
||||
impl<A: Atom> TheoryAtom<A> for SetTheory<A> {
|
||||
type Helper = SetTheoryHelper<A>;
|
||||
|
||||
fn new(atom: A) -> Self {
|
||||
Self(atom)
|
||||
}
|
||||
|
||||
fn new_helper(idx: usize, atom: A) -> Self::Helper {
|
||||
SetTheoryHelper(idx, atom)
|
||||
}
|
||||
}
|
||||
|
|
|
@ -39,4 +39,11 @@ pub enum Problems {
|
|||
/// Will only return the empty extension if no other is found
|
||||
#[clap(visible_alias = "se-ad")]
|
||||
SampleAdmissibility,
|
||||
#[clap(visible_alias = "ee-co")]
|
||||
EnumerateComplete,
|
||||
#[clap(visible_alias = "dc-co")]
|
||||
DecideCredulousComplete {
|
||||
#[arg(long, short = 'a', required = true)]
|
||||
query: u32,
|
||||
},
|
||||
}
|
||||
|
|
16
src/main.rs
16
src/main.rs
|
@ -4,9 +4,12 @@
|
|||
|
||||
use std::{collections::HashSet, fmt::Write as WriteFmt, fs::read_to_string, io::Write as WriteIo};
|
||||
|
||||
use aba::problems::admissibility::{
|
||||
DecideCredulousAdmissibility, EnumerateAdmissibleExtensions, SampleAdmissibleExtension,
|
||||
VerifyAdmissibleExtension,
|
||||
use aba::problems::{
|
||||
admissibility::{
|
||||
DecideCredulousAdmissibility, EnumerateAdmissibleExtensions, SampleAdmissibleExtension,
|
||||
VerifyAdmissibleExtension,
|
||||
},
|
||||
complete::{DecideCredulousComplete, EnumerateCompleteExtensions},
|
||||
};
|
||||
use clap::Parser;
|
||||
|
||||
|
@ -64,6 +67,13 @@ fn __main() -> Result {
|
|||
aba::problems::solve(DecideCredulousAdmissibility { assumption: query }, &aba)?
|
||||
.fmt_iccma()
|
||||
}
|
||||
args::Problems::EnumerateComplete => {
|
||||
aba::problems::multishot_solve(EnumerateCompleteExtensions::default(), &aba)?
|
||||
.fmt_iccma()
|
||||
}
|
||||
args::Problems::DecideCredulousComplete { query } => {
|
||||
aba::problems::solve(DecideCredulousComplete { assumption: query }, &aba)?.fmt_iccma()
|
||||
}
|
||||
}?;
|
||||
let mut stdout = std::io::stdout().lock();
|
||||
match writeln!(stdout, "{}", result) {
|
||||
|
|
Loading…
Reference in a new issue