megamanmalte/aba2sat
0
0
Fork 0
Code Issues Pull requests Packages Projects Releases Wiki Activity

fix memory issues, 2000 atoms, no problem with that!

Browse source 
400 cycles? No issue found!
This commit is contained in:
Malte Tammena 2024-04-18 17:35:18 +02:00
parent 4d89213fc9
commit 3dc977482f
12 changed files with 437 additions and 312 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

236
flake.nix
View file

@ -30,8 +30,17 @@
};
};
outputs = inputs @ { self, nixpkgs, flake-parts, crane, fenix, flake-utils, advisory-db, rust-overlay, }:
flake-parts.lib.mkFlake { inherit inputs self; } {
outputs = inputs @ {
self,
nixpkgs,
flake-parts,
crane,
fenix,
flake-utils,
advisory-db,
rust-overlay,
}:
flake-parts.lib.mkFlake {inherit inputs self;} {
imports = [
];
@ -43,140 +52,155 @@
flake.hydraJobs.devShells.x86_64-linux = self.devShells.x86_64-linux;
flake.hydraJobs.checks.x86_64-linux = self.checks.x86_64-linux;
perSystem =
{ self'
, pkgs
, lib
, config
, system
, ...
}:
let
perSystem = {
self',
pkgs,
lib,
config,
system,
...
}: let
# Load toolchain from file and extend with rust-src and rust-analyzer + clippy
rustToolchain = (pkgs.rust-bin.fromRustupToolchainFile (self + /rust-toolchain.toml)).override {
extensions = [
"rust-src"
"rust-analyzer"
"clippy"
];
};
rustToolchain = pkgs.rust-bin.fromRustupToolchainFile ./rust-toolchain.toml;
# NB: we don't need to overlay our custom toolchain for the *entire*
# pkgs (which would require rebuidling anything else which uses rust).
# Instead, we just want to update the scope that crane will use by appending
# our specific toolchain there.
craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain;
# NB: we don't need to overlay our custom toolchain for the *entire*
# pkgs (which would require rebuidling anything else which uses rust).
# Instead, we just want to update the scope that crane will use by appending
# our specific toolchain there.
craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain;
src = craneLib.cleanCargoSource (craneLib.path ./.);
src = craneLib.cleanCargoSource (craneLib.path ./.);
# Common arguments can be set here to avoid repeating them later
commonArgs = {
inherit src;
strictDeps = true;
# Common arguments can be set here to avoid repeating them later
commonArgs = {
inherit src;
strictDeps = true;
buildInputs = [
buildInputs =
[
# Add additional build inputs here
] ++ lib.optionals pkgs.stdenv.isDarwin [
]
++ lib.optionals pkgs.stdenv.isDarwin [
# Additional darwin specific inputs can be set here
pkgs.libiconv
];
# Additional environment variables can be set directly
# MY_CUSTOM_VAR = "some value";
};
# Additional environment variables can be set directly
# MY_CUSTOM_VAR = "some value";
};
craneLibLLvmTools = craneLib.overrideToolchain
(fenix.packages.${system}.complete.withComponents [
"cargo"
"llvm-tools"
"rustc"
]);
craneLibLLvmTools =
craneLib.overrideToolchain
(fenix.packages.${system}.complete.withComponents [
"cargo"
"llvm-tools"
"rustc"
]);
# Build *just* the cargo dependencies, so we can reuse
# all of that work (e.g. via cachix) when running in CI
cargoArtifacts = craneLib.buildDepsOnly commonArgs;
# Build *just* the cargo dependencies, so we can reuse
# all of that work (e.g. via cachix) when running in CI
cargoArtifacts = craneLib.buildDepsOnly commonArgs;
# Build the actual crate itself, reusing the dependency
# artifacts from above.
aba2sat = craneLib.buildPackage (commonArgs // {
# Build the actual crate itself, reusing the dependency
# artifacts from above.
aba2sat = craneLib.buildPackage (commonArgs
// {
inherit cargoArtifacts;
});
in
{
_module.args.pkgs = import nixpkgs {
inherit system;
overlays = [
(import rust-overlay)
];
};
in {
_module.args.pkgs = import nixpkgs {
inherit system;
overlays = [
(import rust-overlay)
];
};
checks = {
# Build the crate as part of `nix flake check` for convenience
inherit aba2sat;
checks = {
# Build the crate as part of `nix flake check` for convenience
inherit aba2sat;
# Run clippy (and deny all warnings) on the crate source,
# again, reusing the dependency artifacts from above.
#
# Note that this is done as a separate derivation so that
# we can block the CI if there are issues here, but not
# prevent downstream consumers from building our crate by itself.
aba2sat-clippy = craneLib.cargoClippy (commonArgs // {
# Run clippy (and deny all warnings) on the crate source,
# again, reusing the dependency artifacts from above.
#
# Note that this is done as a separate derivation so that
# we can block the CI if there are issues here, but not
# prevent downstream consumers from building our crate by itself.
aba2sat-clippy = craneLib.cargoClippy (commonArgs
// {
inherit cargoArtifacts;
cargoClippyExtraArgs = "--all-targets -- --deny warnings";
});
aba2sat-doc = craneLib.cargoDoc (commonArgs // {
aba2sat-doc = craneLib.cargoDoc (commonArgs
// {
inherit cargoArtifacts;
});
# Check formatting
aba2sat-fmt = craneLib.cargoFmt {
inherit src;
};
# Check formatting
aba2sat-fmt = craneLib.cargoFmt {
inherit src;
};
# Audit dependencies
aba2sat-audit = craneLib.cargoAudit {
inherit src advisory-db;
};
# Audit dependencies
aba2sat-audit = craneLib.cargoAudit {
inherit src advisory-db;
};
# Audit licenses
aba2sat-deny = crane.lib.${system}.cargoDeny {
inherit src;
};
# Audit licenses
aba2sat-deny = crane.lib.${system}.cargoDeny {
inherit src;
};
# Run tests with cargo-nextest
# Consider setting `doCheck = false` on `aba2sat` if you do not want
# the tests to run twice
aba2sat-nextest = craneLib.cargoNextest (commonArgs // {
# Run tests with cargo-nextest
# Consider setting `doCheck = false` on `aba2sat` if you do not want
# the tests to run twice
aba2sat-nextest = craneLib.cargoNextest (commonArgs
// {
inherit cargoArtifacts;
partitions = 1;
partitionType = "count";
});
};
packages = {
default = aba2sat;
aspforaba = pkgs.callPackage ./nix/packages/aspforaba.nix { inherit (self'.packages) clingo; };
clingo = pkgs.callPackage ./nix/packages/clingo.nix { };
} // lib.optionalAttrs (!pkgs.stdenv.isDarwin) {
aba2sat-llvm-coverage = craneLibLLvmTools.cargoLlvmCov (commonArgs // {
inherit cargoArtifacts;
});
};
apps.default = flake-utils.lib.mkApp {
drv = aba2sat;
};
devShells.default = craneLib.devShell {
# Inherit inputs from checks.
checks = self.checks.${system};
RUST_LOG = "trace";
# Extra inputs can be added here; cargo and rustc are provided by default.
packages = [
pkgs.nil
pkgs.pre-commit
pkgs.shellcheck
pkgs.shfmt
pkgs.nodejs
];
};
};
packages =
{
default = aba2sat;
aspforaba = pkgs.callPackage ./nix/packages/aspforaba.nix {inherit (self'.packages) clingo;};
clingo = pkgs.callPackage ./nix/packages/clingo.nix {};
}
// lib.optionalAttrs (!pkgs.stdenv.isDarwin) {
aba2sat-llvm-coverage = craneLibLLvmTools.cargoLlvmCov (commonArgs
// {
inherit cargoArtifacts;
});
};
apps.default = flake-utils.lib.mkApp {
drv = aba2sat;
};
devShells.default = craneLib.devShell {
# Inherit inputs from checks.
checks = self.checks.${system};
RUST_LOG = "trace";
# Extra inputs can be added here; cargo and rustc are provided by default.
packages = [
pkgs.nil
pkgs.pre-commit
pkgs.shellcheck
pkgs.shfmt
pkgs.nodejs
self'.packages.aspforaba
];
};
};
};
}

10
src/aba/debug.rs
View file

@ -41,12 +41,22 @@ impl DebugAba {
self.forward_map.get(&atom).cloned()
}
pub fn backward_atom(&self, atom: Num) -> Option<char> {
self.backward_map.get(&atom).cloned()
}
pub fn forward_set(&self, set: HashSet<char>) -> Option<HashSet<Num>> {
set.into_iter()
.map(|atom| self.forward_atom(atom))
.collect()
}
pub fn backward_set(&self, set: HashSet<Num>) -> Option<HashSet<char>> {
set.into_iter()
.map(|atom| self.backward_atom(atom))
.collect()
}
pub fn forward_sets<S: IntoIterator<Item = HashSet<char>>>(
&self,
sets: S,

46
src/aba/mod.rs
View file

@ -25,13 +25,7 @@
//! // The result should be true
//! assert!(result)
//! ```
use std::{
collections::{HashMap, HashSet},
marker::PhantomData,
num::NonZeroUsize,
};
use crate::literal::TheoryAtom;
use std::collections::{HashMap, HashSet};
use self::prepared::PreparedAba;
@ -40,21 +34,6 @@ mod prepared;
pub mod problems;
mod theory;
#[derive(Debug)]
pub struct Theory(Num);
impl From<Theory> for (Num, Option<NonZeroUsize>) {
fn from(value: Theory) -> Self {
(value.0, None)
}
}
impl From<Num> for Theory {
fn from(value: Num) -> Self {
Self(value)
}
}
pub type Rule = (Num, HashSet<Num>);
pub type RuleList = Vec<Rule>;
pub type Num = u32;
@ -123,26 +102,3 @@ impl Aba {
self.rules.iter().map(|(head, _)| head)
}
}
#[derive(Debug)]
struct TheoryHelper<T: TheoryAtom> {
idx: usize,
atom: Num,
inner: PhantomData<T>,
}
impl<T: TheoryAtom> From<TheoryHelper<T>> for (Num, Option<NonZeroUsize>) {
fn from(value: TheoryHelper<T>) -> Self {
(value.atom, NonZeroUsize::new(value.idx + 1))
}
}
impl<T: TheoryAtom> TheoryHelper<T> {
fn new(idx: usize, atom: Num) -> Self {
Self {
idx,
atom,
inner: PhantomData,
}
}
}

148
src/aba/prepared.rs
View file

@ -11,14 +11,21 @@ use petgraph::{
graph::DiGraph,
};
use crate::{aba::Num, clauses::Clause, literal::TheoryAtom};
use crate::{
aba::Num,
clauses::Clause,
literal::{
lits::{LoopHelper, TheoryRuleBodyActive},
IntoLiteral, RawLiteral,
},
};
use super::{theory::theory_helper, Aba, RuleList};
use super::{theory::theory_helper, Aba};
#[derive(Debug, Clone, PartialEq, Eq)]
struct r#Loop {
heads: HashSet<Num>,
support: RuleList,
support: Vec<usize>,
}
#[derive(Debug, Clone, PartialEq, Eq)]
@ -29,29 +36,119 @@ pub struct PreparedAba {
impl PreparedAba {
/// Translate the ABA into base rules / definitions for SAT solving
pub fn derive_clauses<I: TheoryAtom>(&self) -> impl Iterator<Item = Clause> + '_ {
theory_helper::<I>(self).chain(self.derive_loop_breaker::<I>())
pub fn derive_clauses<
Theory: From<Num> + Into<RawLiteral> + 'static,
Helper: From<(usize, Num)> + Into<RawLiteral> + 'static,
TheoryRuleActive: From<usize> + Into<RawLiteral> + 'static,
>(
&self,
) -> impl Iterator<Item = Clause> + '_ {
theory_helper::<Theory, Helper>(self)
.chain(self.derive_loop_breaker::<Theory>())
.chain(self.derive_rule_helper::<Theory, TheoryRuleActive>())
}
fn derive_loop_breaker<I: TheoryAtom>(&self) -> impl Iterator<Item = Clause> + '_ {
self.loops.iter().flat_map(|r#loop| {
let mut head_list: Vec<_> = r#loop.heads.iter().collect();
head_list.push(head_list[0]);
let body_rules = r#loop.support.iter().map(|(_head, body)| body);
let clauses = body_rules
.multi_cartesian_product()
.flat_map(move |product| {
r#loop.heads.iter().map(move |head| {
product
.iter()
.map(|elem| I::new(**elem).pos())
.chain(std::iter::once(I::new(*head).neg()))
.collect()
})
});
clauses
/// Derive [`Clause`]s to ground the found loops
///
/// Given the loop based on these rules
/// ```text
/// p <- q
/// q <- p
/// q <- a
/// p <- b
/// ```
/// the breaker will derive the formulas
/// ```text
/// p => a v b
/// q => a v b
/// ```
/// or, in the more general case for Loop `L` and incoming rules `Ri = {ri1, ..., rin}`, where all elements of the body of a rule are outside of the loop, we have for all elements `l in L` with id `i`:
/// ```text
/// l => and(body(ri1)) or ... or and(body(rln))
/// ```
/// where body(h <- B) = B and and({a1, ..., ax}) = a1 and ... and ax.
///
/// This will lead to an exponential explosion when converted to naively CNF,
/// since the formulas are mostly DNF. We use Tseitin's transformation to prevent this:
/// ```text
/// LH_i <=> RBA_1 or ... or RBA_n
/// ⋄ (LH_i or -RBA_1) and ... and (LH_i or -RBA_n) and (-LH_i or RBA_1 or ... or RBA_n)
///
/// l => LH_i
/// ⋄ -l or LH_i
/// ```
/// This will result in `|L| + 1` new clauses per loop.
fn derive_loop_breaker<Theory: From<Num> + IntoLiteral>(
&self,
) -> impl Iterator<Item = Clause> + '_ {
// Iterate over all loops
self.loops.iter().enumerate().flat_map(|(loop_id, r#loop)| {
// -LH_i or RBA_1 or ... or RBA_n
let last_clause = r#loop
.support
.iter()
.map(|el| TheoryRuleBodyActive::from(*el).pos())
.chain(std::iter::once(LoopHelper::from(loop_id).neg()))
.collect();
// -l or LH_i
let head_clauses = r#loop.heads.iter().map(move |head| {
Clause::from(vec![
LoopHelper::from(loop_id).pos(),
Theory::from(*head).neg(),
])
});
// LH_i or -RBA_x
let tuple_clauses = r#loop.support.iter().map(move |rule_id| {
Clause::from(vec![
TheoryRuleBodyActive::from(*rule_id).neg(),
LoopHelper::from(loop_id).pos(),
])
});
tuple_clauses.chain([last_clause]).chain(head_clauses)
})
}
/// Derive helper for every rule
///
/// This simplifies some thinks massively and is used by the loop breaker
/// and prevents exponential explosion for rules with the same head.
///
/// For a rule `h <- b_1, ..., b_n with index i in R`, create a helper
/// ```text
/// RBA_i <=> b_1 and ... and b_n
/// ⋄ (-RBA_i or b_1) and ... and (-RBA_i or b_n) and (RBA_i or -b_1 or ... or -b_n)
/// ```
/// we will use [`RuleBodyActive`] for `x_R`.
fn derive_rule_helper<
Theory: From<Num> + Into<RawLiteral> + 'static,
TheoryRuleActive: From<usize> + Into<RawLiteral> + 'static,
>(
&self,
) -> impl Iterator<Item = Clause> + '_ {
self.rules
.iter()
.enumerate()
.flat_map(|(rule_id, (_head, body))| {
if body.is_empty() {
vec![Clause::from(vec![TheoryRuleActive::from(rule_id).neg()])]
} else {
let last_clause = body
.iter()
.map(|el| Theory::from(*el).neg())
.chain(std::iter::once(TheoryRuleActive::from(rule_id).pos()))
.collect();
body.iter()
.map(move |el| {
Clause::from(vec![
TheoryRuleActive::from(rule_id).neg(),
Theory::from(*el).pos(),
])
})
.chain([last_clause])
.collect()
}
})
}
}
/// Filtered list of rules
@ -117,12 +214,13 @@ fn calculate_loops_and_their_support(aba: &Aba) -> Vec<r#Loop> {
let loop_rules = aba
.rules
.iter()
.filter(|(head, _body)| heads.contains(head));
.enumerate()
.filter(|(_rule_id, (head, _body))| heads.contains(head));
// Relevant rules are those that contain only elements from outside the loop
// All other rules cannot influence the value of the loop
let support = loop_rules
.filter(|(_head, body)| body.is_disjoint(&heads))
.cloned()
.filter(|(_rule_id, (_head, body))| body.is_disjoint(&heads))
.map(|(rule_id, _)| rule_id)
.collect();
loops.push(r#Loop { heads, support });
if loops.len() >= (LOOP_SIZE_IN_MULT_UNIVERSE_SIZE * universe.len() as f32) as usize {

56
src/aba/problems/admissibility.rs
View file

@ -2,14 +2,17 @@
use std::collections::HashSet;
use crate::{
aba::{prepared::PreparedAba, Aba, Num, Theory},
aba::{prepared::PreparedAba, Aba, Num},
clauses::{Clause, ClauseList},
error::Error,
literal::{IntoLiteral, TheoryAtom},
literal::{
lits::{Theory, TheorySet, TheorySetHelper, TheorySetRuleBodyActive},
IntoLiteral,
},
Result,
};
use super::{LoopControl, MultishotProblem, Problem, SetTheory, SolverState};
use super::{LoopControl, MultishotProblem, Problem, SolverState};
/// Compute all admissible extensions for an [`Aba`]
#[derive(Default, Debug)]
@ -32,38 +35,37 @@ pub struct DecideCredulousAdmissibility {
pub element: Num,
}
pub fn initial_admissibility_clauses<I: std::fmt::Debug + 'static + TheoryAtom>(
aba: &PreparedAba,
) -> ClauseList {
pub fn initial_admissibility_clauses(aba: &PreparedAba) -> ClauseList {
let mut clauses = vec![];
// Create inference for the problem set
aba.derive_clauses::<I>().collect_into(&mut clauses);
aba.derive_clauses::<TheorySet, TheorySetHelper, TheorySetRuleBodyActive>()
.collect_into(&mut clauses);
// Attack the inference of the aba, if an attack exists
for (assumption, inverse) in &aba.inverses {
[
// For any assumption `a` and it's inverse `b`:
// a in th(A) <=> b not in th(S)
Clause::from(vec![
Theory::new(*assumption).pos(),
SetTheory::new(*inverse).pos(),
Theory::from(*assumption).pos(),
TheorySet::from(*inverse).pos(),
]),
Clause::from(vec![
Theory::new(*assumption).neg(),
SetTheory::new(*inverse).neg(),
Theory::from(*assumption).neg(),
TheorySet::from(*inverse).neg(),
]),
// Prevent attacks from the opponent to the selected set
// For any assumption `a` and it's inverse `b`:
// b in th(A) and a in th(S) => bottom
Clause::from(vec![
Theory::new(*inverse).neg(),
SetTheory::new(*assumption).neg(),
Theory::from(*inverse).neg(),
TheorySet::from(*assumption).neg(),
]),
// Prevent self-attacks
// For any assumption `a` and it's inverse `b`:
// a in th(S) and b in th(S) => bottom
Clause::from(vec![
SetTheory::new(*assumption).neg(),
SetTheory::new(*inverse).neg(),
TheorySet::from(*assumption).neg(),
TheorySet::from(*inverse).neg(),
]),
]
.into_iter()
@ -77,7 +79,7 @@ fn construct_found_set(state: SolverState<'_>) -> HashSet<Num> {
.aba
.assumptions()
.filter_map(|assumption| {
let literal = SetTheory::new(*assumption).pos();
let literal = TheorySet::from(*assumption).pos();
let raw = state.map.get_raw(&literal)?;
match state.solver.value(raw) {
Some(true) => Some(*assumption),
@ -91,12 +93,12 @@ impl Problem for SampleAdmissibleExtension {
type Output = HashSet<Num>;
fn additional_clauses(&self, aba: &PreparedAba) -> ClauseList {
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
let mut clauses = initial_admissibility_clauses(aba);
// Prevent the empty set
let no_empty_set: Clause = aba
.inverses
.keys()
.map(|assumption| SetTheory::new(*assumption).pos())
.map(|assumption| TheorySet::from(*assumption).pos())
.collect();
clauses.push(no_empty_set);
clauses
@ -117,12 +119,12 @@ impl MultishotProblem for EnumerateAdmissibleExtensions {
fn additional_clauses(&self, aba: &PreparedAba, iteration: usize) -> ClauseList {
match iteration {
0 => {
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
let mut clauses = initial_admissibility_clauses(aba);
// Prevent the empty set
let no_empty_set: Clause = aba
.inverses
.keys()
.map(|assumption| SetTheory::new(*assumption).pos())
.map(|assumption| TheorySet::from(*assumption).pos())
.collect();
clauses.push(no_empty_set);
clauses
@ -136,9 +138,9 @@ impl MultishotProblem for EnumerateAdmissibleExtensions {
.assumptions()
.map(|assumption| {
if just_found.contains(assumption) {
SetTheory::new(*assumption).neg()
TheorySet::from(*assumption).neg()
} else {
SetTheory::new(*assumption).pos()
TheorySet::from(*assumption).pos()
}
})
.collect();
@ -157,7 +159,7 @@ impl MultishotProblem for EnumerateAdmissibleExtensions {
.inverses
.keys()
.filter_map(|assumption| {
let literal = SetTheory::new(*assumption).pos();
let literal = TheorySet::from(*assumption).pos();
let raw = state.map.get_raw(&literal)?;
match state.solver.value(raw) {
Some(true) => Some(*assumption),
@ -187,10 +189,10 @@ impl Problem for VerifyAdmissibleExtension {
type Output = bool;
fn additional_clauses(&self, aba: &PreparedAba) -> crate::clauses::ClauseList {
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
let mut clauses = initial_admissibility_clauses(aba);
// Force inference on all members of the set
for assumption in aba.assumptions() {
let inf = SetTheory::new(*assumption);
let inf = TheorySet::from(*assumption);
if self.assumptions.contains(assumption) {
clauses.push(Clause::from(vec![inf.pos()]))
} else {
@ -223,8 +225,8 @@ impl Problem for DecideCredulousAdmissibility {
type Output = bool;
fn additional_clauses(&self, aba: &PreparedAba) -> ClauseList {
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
clauses.push(Clause::from(vec![SetTheory(self.element).pos()]));
let mut clauses = initial_admissibility_clauses(aba);
clauses.push(Clause::from(vec![TheorySet::from(self.element).pos()]));
clauses
}

23
src/aba/problems/complete.rs
View file

@ -1,16 +1,19 @@
use std::collections::HashSet;
use crate::{
aba::{prepared::PreparedAba, Aba, Num, Theory},
aba::{prepared::PreparedAba, Aba, Num},
clauses::{Clause, ClauseList},
error::Error,
literal::{IntoLiteral, TheoryAtom},
literal::{
lits::{Theory, TheorySet},
IntoLiteral,
},
Result,
};
use super::{
admissibility::initial_admissibility_clauses, LoopControl, MultishotProblem, Problem,
SetTheory, SolverState,
SolverState,
};
#[derive(Debug, Default)]
@ -25,14 +28,14 @@ pub struct DecideCredulousComplete {
fn initial_complete_clauses(aba: &PreparedAba) -> ClauseList {
// Take everything from admissibility
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
let mut clauses = initial_admissibility_clauses(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).pos(),
SetTheory(*assumption).pos(),
Theory::from(*inverse).pos(),
TheorySet::from(*assumption).pos(),
]));
}
clauses
@ -53,9 +56,9 @@ impl MultishotProblem for EnumerateCompleteExtensions {
.assumptions()
.map(|assumption| {
if just_found.contains(assumption) {
SetTheory::new(*assumption).neg()
TheorySet::from(*assumption).neg()
} else {
SetTheory::new(*assumption).pos()
TheorySet::from(*assumption).pos()
}
})
.collect();
@ -74,7 +77,7 @@ impl MultishotProblem for EnumerateCompleteExtensions {
.inverses
.keys()
.filter_map(|assumption| {
let literal = SetTheory::new(*assumption).pos();
let literal = TheorySet::from(*assumption).pos();
let raw = state.map.get_raw(&literal)?;
match state.solver.value(raw) {
Some(true) => Some(*assumption),
@ -96,7 +99,7 @@ impl Problem for DecideCredulousComplete {
fn additional_clauses(&self, aba: &PreparedAba) -> ClauseList {
let mut clauses = initial_complete_clauses(aba);
clauses.push(Clause::from(vec![SetTheory(self.element).pos()]));
clauses.push(Clause::from(vec![TheorySet::from(self.element).pos()]));
clauses
}

10
src/aba/problems/conflict_free.rs
View file

@ -1,10 +1,10 @@
use std::collections::HashSet;
use crate::{
aba::{prepared::PreparedAba, Aba, Num, Theory},
aba::{prepared::PreparedAba, Aba, Num},
clauses::{Clause, ClauseList},
error::Error,
literal::{IntoLiteral, TheoryAtom},
literal::{lits::Theory, IntoLiteral},
Result,
};
@ -21,7 +21,7 @@ impl Problem for ConflictFreeness {
let mut clauses = vec![];
// Make sure that every assumption in our problem is inferred and every other not
for assumption in aba.assumptions() {
let theory = Theory::new(*assumption);
let theory = Theory::from(*assumption);
if self.assumptions.contains(assumption) {
clauses.push(vec![theory.pos()].into())
} else {
@ -30,8 +30,8 @@ impl Problem for ConflictFreeness {
}
for (assumption, inverse) in &aba.inverses {
clauses.push(Clause::from(vec![
Theory::new(*assumption).neg(),
Theory::new(*inverse).neg(),
Theory::from(*assumption).neg(),
Theory::from(*inverse).neg(),
]));
}
clauses

29
src/aba/problems/mod.rs
View file

@ -1,14 +1,13 @@
use std::num::NonZeroUsize;
use cadical::Solver;
use crate::{
clauses::ClauseList,
error::{Error, Result},
literal::lits::{Theory, TheoryHelper, TheoryRuleBodyActive},
mapper::Mapper,
};
use super::{prepared::PreparedAba, Aba, Num, Theory};
use super::{prepared::PreparedAba, Aba};
pub mod admissibility;
pub mod complete;
@ -50,22 +49,6 @@ pub trait MultishotProblem {
}
}
/// *(Literal)* `A` is element of `th(S)`
#[derive(Debug)]
pub struct SetTheory(Num);
impl From<SetTheory> for (Num, Option<NonZeroUsize>) {
fn from(value: SetTheory) -> Self {
(value.0, None)
}
}
impl From<Num> for SetTheory {
fn from(value: Num) -> Self {
Self(value)
}
}
pub fn solve<P: Problem>(problem: P, aba: Aba) -> Result<P::Output> {
let aba = aba.prepare();
// Let the problem perform additional checks before starting the solver
@ -76,7 +59,9 @@ pub fn solve<P: Problem>(problem: P, aba: Aba) -> Result<P::Output> {
// Instantiate a new SAT solver instance
let mut sat: Solver = Solver::default();
// Derive clauses from the ABA
let clauses: ClauseList = aba.derive_clauses::<Theory>().collect();
let clauses: ClauseList = aba
.derive_clauses::<Theory, TheoryHelper, TheoryRuleBodyActive>()
.collect();
// Append additional clauses as defined by the problem
let additional_clauses = problem.additional_clauses(&aba);
// Convert the total of our derived clauses using the mapper
@ -116,7 +101,9 @@ pub fn multishot_solve<P: MultishotProblem>(mut problem: P, aba: Aba) -> Result<
// Instantiate a new SAT solver instance
let mut sat: Solver = Solver::default();
// Derive clauses from the ABA
let clauses: ClauseList = aba.derive_clauses::<Theory>().collect();
let clauses: ClauseList = aba
.derive_clauses::<Theory, TheoryHelper, TheoryRuleBodyActive>()
.collect();
// Convert the total of our derived clauses using the mapper
// and feed the solver with the result
map.as_raw_iter(&clauses)

32
src/aba/theory.rs
View file

@ -2,10 +2,10 @@ use std::collections::{HashMap, HashSet};
use crate::{
clauses::{Clause, ClauseList},
literal::{IntoLiteral, Literal, TheoryAtom},
literal::{IntoLiteral, Literal, RawLiteral},
};
use super::{prepared::PreparedAba, Num, TheoryHelper};
use super::{prepared::PreparedAba, Num};
/// Generate the logic for theory derivation in the given [`Aba`]
///
@ -32,7 +32,12 @@ use super::{prepared::PreparedAba, Num, TheoryHelper};
/// A lot of the overhead is due to the fact that multiple bodies are an option, if that's
/// not given for a head `p` we use the simplified translation logic where `p` is true iff
/// `bodies(p)` is true.
pub fn theory_helper<I: TheoryAtom>(aba: &PreparedAba) -> impl Iterator<Item = Clause> + '_ {
pub fn theory_helper<
Theory: From<Num> + Into<RawLiteral>,
Helper: From<(usize, Num)> + Into<RawLiteral>,
>(
aba: &PreparedAba,
) -> impl Iterator<Item = Clause> + '_ {
// The combined list of rules, such that every
// head is unique and possible contains a list of bodies
let mut rules_combined =
@ -59,10 +64,10 @@ pub fn theory_helper<I: TheoryAtom>(aba: &PreparedAba) -> impl Iterator<Item = C
.flat_map(|(head, bodies)| match &bodies[..] {
// No bodies, add a clause that prevents the head from accuring in the theory
[] => {
vec![Clause::from(vec![I::new(*head).neg()])]
vec![Clause::from(vec![Theory::from(*head).neg()])]
}
// A single body only, this is equivalent to a head that can only be derived by a single rule
[body] => body_to_clauses::<I>(I::new(*head).pos(), body),
[body] => body_to_clauses::<Theory>(Theory::from(*head).pos(), body),
// n bodies, we'll need to take extra care to allow any number of bodies to derive this
// head without logic errors
bodies => {
@ -71,31 +76,34 @@ pub fn theory_helper<I: TheoryAtom>(aba: &PreparedAba) -> impl Iterator<Item = C
.iter()
.enumerate()
.flat_map(|(idx, body)| {
body_to_clauses::<I>(TheoryHelper::<I>::new(idx, *head).pos(), body)
body_to_clauses::<Theory>(Helper::from((idx, *head)).pos(), body)
})
.collect_into(&mut clauses);
let helpers: Vec<_> = (0..bodies.len())
.map(|idx| TheoryHelper::<I>::new(idx, *head).pos())
.map(|idx| Helper::from((idx, *head)).pos())
.collect();
let mut right_implification: Clause = helpers.iter().cloned().collect();
right_implification.push(I::new(*head).neg());
right_implification.push(Theory::from(*head).neg());
clauses.push(right_implification);
helpers
.into_iter()
.map(|helper| Clause::from(vec![I::new(*head).pos(), helper.negative()]))
.map(|helper| Clause::from(vec![Theory::from(*head).pos(), helper.negative()]))
.collect_into(&mut clauses);
clauses
}
})
}
fn body_to_clauses<I: TheoryAtom>(head: Literal, body: &HashSet<Num>) -> ClauseList {
fn body_to_clauses<Theory: From<Num> + Into<RawLiteral>>(
head: Literal,
body: &HashSet<Num>,
) -> ClauseList {
let mut clauses = vec![];
let mut left_implication: Clause = body.iter().map(|elem| I::new(*elem).neg()).collect();
let mut left_implication: Clause = body.iter().map(|elem| Theory::from(*elem).neg()).collect();
left_implication.push(head.clone().positive());
clauses.push(left_implication);
body.iter()
.map(|elem| vec![head.clone().negative(), I::new(*elem).pos()].into())
.map(|elem| vec![head.clone().negative(), Theory::from(*elem).pos()].into())
.collect_into(&mut clauses);
clauses
}

125
src/literal.rs
View file

@ -1,10 +1,73 @@
use std::{
any::{Any, TypeId},
fmt::Debug,
num::NonZeroUsize,
};
use std::fmt::Debug;
use crate::aba::Num;
pub mod lits {
use crate::aba::Num;
macro_rules! into_raw {
($ty:ident) => {
impl From<$ty> for crate::literal::RawLiteral {
fn from(value: $ty) -> crate::literal::RawLiteral {
crate::literal::RawLiteral::$ty(value)
}
}
};
($ty:ident from $other:ident) => {
impl From<$ty> for crate::literal::RawLiteral {
fn from(value: $ty) -> crate::literal::RawLiteral {
crate::literal::RawLiteral::$ty(value)
}
}
impl From<$other> for $ty {
fn from(value: $other) -> Self {
Self(value)
}
}
};
($ty:ident from $( $other:ident ),+ ) => {
impl From<$ty> for crate::literal::RawLiteral {
fn from(value: $ty) -> crate::literal::RawLiteral {
crate::literal::RawLiteral::$ty(value)
}
}
#[allow(non_snake_case)]
impl From<($( $other ,)+)> for $ty {
fn from(($( $other ),+): ($( $other ),+)) -> Self {
Self($( $other ),+)
}
}
};
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct Theory(Num);
into_raw!(Theory from Num);
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct TheoryHelper(usize, Num);
into_raw!(TheoryHelper from usize, Num);
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct TheoryRuleBodyActive(usize);
into_raw!(TheoryRuleBodyActive from usize);
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct TheorySet(Num);
into_raw!(TheorySet from Num);
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct TheorySetHelper(usize, Num);
into_raw!(TheorySetHelper from usize, Num);
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct TheorySetRuleBodyActive(usize);
into_raw!(TheorySetRuleBodyActive from usize);
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct LoopHelper(usize);
into_raw!(LoopHelper from usize);
}
/// A Literal can be used in SAT [`Clause`](crate::clauses::Clause)s
#[derive(Clone)]
@ -13,9 +76,20 @@ pub enum Literal {
Neg(RawLiteral),
}
/// New type to prevent creation of arbitrary SAT literals
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct RawLiteral(TypeId, Num, Option<NonZeroUsize>);
/// All SAT-encodable literals
///
/// This is a single type to ease memory and logic, at the cost of having to
/// extend this type for every new literal type
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum RawLiteral {
Theory(lits::Theory),
TheoryHelper(lits::TheoryHelper),
TheoryRuleBodyActive(lits::TheoryRuleBodyActive),
TheorySet(lits::TheorySet),
TheorySetHelper(lits::TheorySetHelper),
TheorySetRuleBodyActive(lits::TheorySetRuleBodyActive),
LoopHelper(lits::LoopHelper),
}
/// Convert the type into it's literal
#[doc(notable_trait)]
@ -32,25 +106,10 @@ pub trait IntoLiteral: Sized {
}
}
/// Implement [`IntoLiteral`] for all types that are 'static, sized and debuggable
impl<T: Any + Into<(Num, Option<NonZeroUsize>)>> IntoLiteral for T {
/// Implement [`IntoLiteral`] for all types that can be converted into [`RawLiteral`]s.
impl<T: Into<RawLiteral>> IntoLiteral for T {
fn into_literal(self) -> RawLiteral {
let (num, index) = self.into();
RawLiteral(TypeId::of::<T>(), num, index)
}
}
/// ([`Literal`]) A literal that can be used to construct the logic behind
/// the theory of a (sub-)set of assumptions (`th(S)`) in an [`Aba`](crate::aba::Aba).
///
/// See [`crate::aba::theory_helper`].
pub trait TheoryAtom: Sized + IntoLiteral + std::fmt::Debug + 'static {
fn new(atom: Num) -> Self;
}
impl<T: From<Num> + Sized + IntoLiteral + std::fmt::Debug + 'static> TheoryAtom for T {
fn new(atom: Num) -> Self {
Self::from(atom)
self.into()
}
}
@ -83,16 +142,8 @@ impl std::ops::Deref for Literal {
impl std::fmt::Debug for Literal {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
Literal::Pos(str) => write!(f, "+{str:?}"),
Literal::Neg(str) => write!(f, "-{str:?}"),
Literal::Pos(inner) => write!(f, "+{inner:?}"),
Literal::Neg(inner) => write!(f, "-{inner:?}"),
}
}
}
// impl std::ops::Deref for RawLiteral {
// type Target = String;
// fn deref(&self) -> &Self::Target {
// &self.0
// }
// }

25
src/mapper.rs
View file

@ -12,11 +12,6 @@ pub struct Mapper {
map: HashMap<RawLiteral, u32>,
}
pub enum ReconstructedLiteral {
Pos(RawLiteral),
Neg(RawLiteral),
}
impl Mapper {
pub fn new() -> Self {
Mapper {
@ -37,7 +32,7 @@ impl Mapper {
let key = self.map.get(lit).copied().unwrap_or_else(|| {
debug_assert!(self.map.len() <= i32::MAX as usize, "Mapper overflowed");
let new = self.map.len() as u32 + 1;
self.map.insert((**lit).clone(), new);
self.map.insert(**lit, new);
new
}) as i32;
match lit {
@ -46,14 +41,11 @@ impl Mapper {
}
}
pub fn reconstruct<'s>(
&'s self,
sat: &'s Solver,
) -> impl Iterator<Item = ReconstructedLiteral> + 's {
pub fn reconstruct<'s>(&'s self, sat: &'s Solver) -> impl Iterator<Item = Literal> + 's {
self.map.iter().flat_map(|(lit, raw)| {
sat.value(*raw as i32).map(|result| match result {
true => ReconstructedLiteral::Pos(lit.clone()),
false => ReconstructedLiteral::Neg(lit.clone()),
true => Literal::Pos(*lit),
false => Literal::Neg(*lit),
})
})
}
@ -62,12 +54,3 @@ impl Mapper {
self.map.get(lit).map(|&raw| raw as i32)
}
}
impl std::fmt::Debug for ReconstructedLiteral {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
ReconstructedLiteral::Pos(str) => write!(f, "+{str:?}"),
ReconstructedLiteral::Neg(str) => write!(f, "-{str:?}"),
}
}
}

9
src/tests/mod.rs
View file

@ -87,7 +87,8 @@ fn simple_admissible_example() {
for elem in aba.forward_sets(expected.clone()).unwrap() {
assert!(
result.contains(&elem),
"{elem:?} was expected but not found in result"
"{:?} was expected but not found in result",
aba.backward_set(elem).unwrap()
);
}
for elem in aba.backward_sets(result).unwrap() {
@ -117,7 +118,8 @@ fn simple_admissible_example_with_defense() {
for elem in aba.forward_sets(expected.clone()).unwrap() {
assert!(
result.contains(&elem),
"{elem:?} was expected but not found in result"
"{:?} was expected but not found in result",
aba.backward_set(elem).unwrap()
);
}
for elem in aba.backward_sets(result).unwrap() {
@ -146,7 +148,8 @@ fn simple_admissible_atomic() {
for elem in aba.forward_sets(expected.clone()).unwrap() {
assert!(
result.contains(&elem),
"{elem:?} was expected but not found in result"
"{:?} was expected but not found in result",
aba.backward_set(elem).unwrap()
);
}
for elem in aba.backward_sets(result).unwrap() {