Kinda working
This commit is contained in:
248
Cargo.lock
generated
248
Cargo.lock
generated
@ -67,6 +67,12 @@ version = "1.5.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8"
|
||||
|
||||
[[package]]
|
||||
name = "bitflags"
|
||||
version = "2.10.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "812e12b5285cc515a9c72a5c1d3b6d46a19dac5acfef5265968c166106e31dd3"
|
||||
|
||||
[[package]]
|
||||
name = "cfg-if"
|
||||
version = "1.0.4"
|
||||
@ -79,6 +85,15 @@ version = "1.0.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b05b61dc5112cbb17e4b6cd61790d9845d13888356391624cbe7e41efeac1e75"
|
||||
|
||||
[[package]]
|
||||
name = "convert_case"
|
||||
version = "0.10.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "633458d4ef8c78b72454de2d54fd6ab2e60f9e02be22f3c6104cdc8a4e0fceb9"
|
||||
dependencies = [
|
||||
"unicode-segmentation",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "corosensei"
|
||||
version = "0.3.2"
|
||||
@ -92,6 +107,64 @@ dependencies = [
|
||||
"windows-sys 0.59.0",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "crossterm"
|
||||
version = "0.29.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d8b9f2e4c67f833b660cdb0a3523065869fb35570177239812ed4c905aeff87b"
|
||||
dependencies = [
|
||||
"bitflags",
|
||||
"crossterm_winapi",
|
||||
"derive_more",
|
||||
"document-features",
|
||||
"mio",
|
||||
"parking_lot",
|
||||
"rustix",
|
||||
"signal-hook",
|
||||
"signal-hook-mio",
|
||||
"winapi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "crossterm_winapi"
|
||||
version = "0.9.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "acdd7c62a3665c7f6830a51635d9ac9b23ed385797f70a83bb8bafe9c572ab2b"
|
||||
dependencies = [
|
||||
"winapi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "derive_more"
|
||||
version = "2.1.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d751e9e49156b02b44f9c1815bcb94b984cdcc4396ecc32521c739452808b134"
|
||||
dependencies = [
|
||||
"derive_more-impl",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "derive_more-impl"
|
||||
version = "2.1.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "799a97264921d8623a957f6c3b9011f3b5492f557bbb7a5a19b7fa6d06ba8dcb"
|
||||
dependencies = [
|
||||
"convert_case",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"rustc_version",
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "document-features"
|
||||
version = "0.2.12"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d4b8a88685455ed29a21542a33abd9cb6510b6b129abadabdcef0f4c55bc8f61"
|
||||
dependencies = [
|
||||
"litrs",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "env_filter"
|
||||
version = "0.1.4"
|
||||
@ -115,6 +188,16 @@ dependencies = [
|
||||
"log",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "errno"
|
||||
version = "0.3.14"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb"
|
||||
dependencies = [
|
||||
"libc",
|
||||
"windows-sys 0.61.2",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "is_terminal_polyfill"
|
||||
version = "1.70.2"
|
||||
@ -151,6 +234,27 @@ version = "0.2.180"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "bcc35a38544a891a5f7c865aca548a982ccb3b8650a5b06d0fd33a10283c56fc"
|
||||
|
||||
[[package]]
|
||||
name = "linux-raw-sys"
|
||||
version = "0.11.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "df1d3c3b53da64cf5760482273a98e575c651a67eec7f77df96b5b642de8f039"
|
||||
|
||||
[[package]]
|
||||
name = "litrs"
|
||||
version = "1.0.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "11d3d7f243d5c5a8b9bb5d6dd2b1602c0cb0b9db1621bafc7ed66e35ff9fe092"
|
||||
|
||||
[[package]]
|
||||
name = "lock_api"
|
||||
version = "0.4.14"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "224399e74b87b5f3557511d98dff8b14089b3dadafcab6bb93eab67d3aace965"
|
||||
dependencies = [
|
||||
"scopeguard",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "log"
|
||||
version = "0.4.29"
|
||||
@ -163,11 +267,24 @@ version = "2.8.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f8ca58f447f06ed17d5fc4043ce1b10dd205e060fb3ce5b979b8ed8e59ff3f79"
|
||||
|
||||
[[package]]
|
||||
name = "mio"
|
||||
version = "1.1.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a69bcab0ad47271a0234d9422b131806bf3968021e5dc9328caf2d4cd58557fc"
|
||||
dependencies = [
|
||||
"libc",
|
||||
"log",
|
||||
"wasi",
|
||||
"windows-sys 0.61.2",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "nanolog"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"corosensei",
|
||||
"crossterm",
|
||||
"env_logger",
|
||||
"log",
|
||||
"winnow",
|
||||
@ -179,6 +296,29 @@ version = "1.70.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe"
|
||||
|
||||
[[package]]
|
||||
name = "parking_lot"
|
||||
version = "0.12.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "93857453250e3077bd71ff98b6a65ea6621a19bb0f559a85248955ac12c45a1a"
|
||||
dependencies = [
|
||||
"lock_api",
|
||||
"parking_lot_core",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "parking_lot_core"
|
||||
version = "0.9.12"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2621685985a2ebf1c516881c026032ac7deafcda1a2c9b7850dc81e3dfcb64c1"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"libc",
|
||||
"redox_syscall",
|
||||
"smallvec",
|
||||
"windows-link",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "portable-atomic"
|
||||
version = "1.13.1"
|
||||
@ -212,6 +352,15 @@ dependencies = [
|
||||
"proc-macro2",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "redox_syscall"
|
||||
version = "0.5.18"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ed2bf2547551a7053d6fdfafda3f938979645c44812fbfcda098faae3f1a362d"
|
||||
dependencies = [
|
||||
"bitflags",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "regex"
|
||||
version = "1.12.3"
|
||||
@ -241,12 +390,40 @@ version = "0.8.9"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a96887878f22d7bad8a3b6dc5b7440e0ada9a245242924394987b21cf2210a4c"
|
||||
|
||||
[[package]]
|
||||
name = "rustc_version"
|
||||
version = "0.4.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92"
|
||||
dependencies = [
|
||||
"semver",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rustix"
|
||||
version = "1.1.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "146c9e247ccc180c1f61615433868c99f3de3ae256a30a43b49f67c2d9171f34"
|
||||
dependencies = [
|
||||
"bitflags",
|
||||
"errno",
|
||||
"libc",
|
||||
"linux-raw-sys",
|
||||
"windows-sys 0.61.2",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "scopeguard"
|
||||
version = "1.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
|
||||
|
||||
[[package]]
|
||||
name = "semver"
|
||||
version = "1.0.27"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d767eb0aabc880b29956c35734170f26ed551a859dbd361d140cdbeca61ab1e2"
|
||||
|
||||
[[package]]
|
||||
name = "serde_core"
|
||||
version = "1.0.228"
|
||||
@ -267,6 +444,43 @@ dependencies = [
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "signal-hook"
|
||||
version = "0.3.18"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d881a16cf4426aa584979d30bd82cb33429027e42122b169753d6ef1085ed6e2"
|
||||
dependencies = [
|
||||
"libc",
|
||||
"signal-hook-registry",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "signal-hook-mio"
|
||||
version = "0.2.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b75a19a7a740b25bc7944bdee6172368f988763b744e3d4dfe753f6b4ece40cc"
|
||||
dependencies = [
|
||||
"libc",
|
||||
"mio",
|
||||
"signal-hook",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "signal-hook-registry"
|
||||
version = "1.4.8"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "c4db69cba1110affc0e9f7bcd48bbf87b3f4fc7c61fc9155afd4c469eb3d6c1b"
|
||||
dependencies = [
|
||||
"errno",
|
||||
"libc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "smallvec"
|
||||
version = "1.15.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03"
|
||||
|
||||
[[package]]
|
||||
name = "syn"
|
||||
version = "2.0.114"
|
||||
@ -284,12 +498,46 @@ version = "1.0.22"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9312f7c4f6ff9069b165498234ce8be658059c6728633667c526e27dc2cf1df5"
|
||||
|
||||
[[package]]
|
||||
name = "unicode-segmentation"
|
||||
version = "1.12.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f6ccf251212114b54433ec949fd6a7841275f9ada20dddd2f29e9ceea4501493"
|
||||
|
||||
[[package]]
|
||||
name = "utf8parse"
|
||||
version = "0.2.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821"
|
||||
|
||||
[[package]]
|
||||
name = "wasi"
|
||||
version = "0.11.1+wasi-snapshot-preview1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b"
|
||||
|
||||
[[package]]
|
||||
name = "winapi"
|
||||
version = "0.3.9"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419"
|
||||
dependencies = [
|
||||
"winapi-i686-pc-windows-gnu",
|
||||
"winapi-x86_64-pc-windows-gnu",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "winapi-i686-pc-windows-gnu"
|
||||
version = "0.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
|
||||
|
||||
[[package]]
|
||||
name = "winapi-x86_64-pc-windows-gnu"
|
||||
version = "0.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
|
||||
|
||||
[[package]]
|
||||
name = "windows-link"
|
||||
version = "0.2.1"
|
||||
|
||||
@ -5,6 +5,7 @@ edition = "2024"
|
||||
|
||||
[dependencies]
|
||||
corosensei = "0.3.2"
|
||||
crossterm = "0.29.0"
|
||||
env_logger = "0.11.8"
|
||||
log = "0.4.29"
|
||||
winnow = "0.7.14"
|
||||
|
||||
29
src/main.rs
29
src/main.rs
@ -1,12 +1,12 @@
|
||||
use corosensei::Coroutine;
|
||||
use nanolog::ast::Body;
|
||||
use nanolog::ast::Module;
|
||||
use nanolog::ast::Predicate;
|
||||
use nanolog::prover::Constraints;
|
||||
|
||||
fn main()
|
||||
{
|
||||
env_logger::builder()
|
||||
.filter_level(log::LevelFilter::Info)
|
||||
.filter_level(log::LevelFilter::Debug)
|
||||
.format_timestamp(None)
|
||||
.format_module_path(false)
|
||||
.init();
|
||||
@ -16,21 +16,32 @@ fn main()
|
||||
integer(s(X)) :- integer(X).
|
||||
add(X, zero, X).
|
||||
add(X, s(Y), Z) :- add(s(X), Y, Z).
|
||||
mult(zero, X, zero).
|
||||
mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z).
|
||||
|
||||
"
|
||||
.into();
|
||||
|
||||
// let a: Predicate = "integer(s(zero))".into();
|
||||
// let a: Predicate = "integer(s(Y))".into();
|
||||
// let b: Predicate = "integer(s(X))".into();
|
||||
//
|
||||
// println!("{:?}", a.unify(&b));
|
||||
// println!("{}", a.unify(&b).unwrap());
|
||||
|
||||
let body: Body = "add(s(s(zero)), s(zero), s(s(s(zero))))".into();
|
||||
let body: Body = "add(s(zero), s(zero), X).".into();
|
||||
body.prove_in_module(&module).next().next();
|
||||
|
||||
// let body: Body = "integer(X).".into();
|
||||
// let body: Body = "add(s(s(zero)), s(zero), s(s(s(zero))))".into();
|
||||
// let body: Body = "add(s(zero), s(zero), X).".into();
|
||||
// body.prove_in_module(&module).next().next();
|
||||
//
|
||||
|
||||
let body: Body = "mult(s(zero), s(s(zero)), X)".into();
|
||||
let mut prover = body.prove_in_module(&module, Constraints::default());
|
||||
while let Some(c) = prover.prove()
|
||||
{
|
||||
println!("{}", c.simplified());
|
||||
//println!("{}", c);
|
||||
|
||||
let _ = std::io::stdin().read_line(&mut String::new());
|
||||
}
|
||||
//
|
||||
//println!("{}", module);
|
||||
//
|
||||
}
|
||||
|
||||
290
src/prover.rs
290
src/prover.rs
@ -1,31 +1,32 @@
|
||||
use std::cell::Cell;
|
||||
use std::cell::RefCell;
|
||||
use std::collections::HashMap;
|
||||
use std::fmt::Display;
|
||||
use std::fmt::write;
|
||||
use std::ops;
|
||||
use std::ops::Rem;
|
||||
use std::rc::Rc;
|
||||
|
||||
use corosensei::Coroutine;
|
||||
use corosensei::Yielder;
|
||||
use log::debug;
|
||||
use log::info;
|
||||
use log::warn;
|
||||
|
||||
use crate::ast::Body;
|
||||
use crate::ast::Clause;
|
||||
use crate::ast::Module;
|
||||
use crate::ast::Predicate;
|
||||
use crate::prover;
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Constraint
|
||||
pub struct Constraints
|
||||
{
|
||||
variable: String,
|
||||
predicate: Predicate,
|
||||
set: HashMap<String, Predicate>,
|
||||
}
|
||||
|
||||
struct Context<'a, 'b>
|
||||
{
|
||||
module: &'a Module,
|
||||
yielder: &'b Yielder<(), Vec<Constraint>>,
|
||||
yielder: &'b Yielder<(), Constraints>,
|
||||
depth: usize,
|
||||
global_counter: Rc<Cell<usize>>,
|
||||
}
|
||||
@ -45,36 +46,55 @@ impl Context<'_, '_>
|
||||
|
||||
pub struct Prover
|
||||
{
|
||||
coroutine: Coroutine<(), Vec<Constraint>, ()>,
|
||||
coroutine: Option<Coroutine<(), Constraints, ()>>,
|
||||
}
|
||||
|
||||
impl Prover
|
||||
{
|
||||
pub fn next(mut self) -> Prover
|
||||
pub fn prove(&mut self) -> Option<Constraints>
|
||||
{
|
||||
self.coroutine.resume(());
|
||||
self
|
||||
if let Some(coroutine) = self.coroutine.as_mut()
|
||||
{
|
||||
match coroutine.resume(())
|
||||
{
|
||||
corosensei::CoroutineResult::Yield(constraints) => Some(constraints),
|
||||
corosensei::CoroutineResult::Return(_) =>
|
||||
{
|
||||
self.coroutine = None;
|
||||
None
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
None
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Body
|
||||
{
|
||||
pub fn prove_in_module(&self, module: &Module) -> Prover
|
||||
pub fn prove_in_module(&self, module: &Module, constraints: Constraints) -> Prover
|
||||
{
|
||||
let cloned_body = self.clone();
|
||||
let cloned_module = module.clone();
|
||||
let coroutine = Coroutine::new(move |yielder, ()| {
|
||||
cloned_body.prove(Context {
|
||||
module: &cloned_module,
|
||||
depth: 0,
|
||||
yielder,
|
||||
global_counter: Rc::new(Cell::new(0)),
|
||||
});
|
||||
cloned_body.prove(
|
||||
Context {
|
||||
module: &cloned_module,
|
||||
depth: 0,
|
||||
yielder,
|
||||
global_counter: Rc::new(Cell::new(0)),
|
||||
},
|
||||
&constraints,
|
||||
);
|
||||
});
|
||||
Prover { coroutine }
|
||||
Prover {
|
||||
coroutine: Some(coroutine),
|
||||
}
|
||||
}
|
||||
|
||||
fn prove(&self, context: Context<'_, '_>)
|
||||
fn prove(&self, context: Context<'_, '_>, constraints: &Constraints)
|
||||
{
|
||||
match self
|
||||
{
|
||||
@ -85,24 +105,41 @@ impl Body
|
||||
predicate.prove_with_clause(
|
||||
&candidate.unique(context.global_counter.clone()),
|
||||
context.descend(),
|
||||
constraints,
|
||||
);
|
||||
}
|
||||
}
|
||||
Body::And(x) => x.iter().for_each(|x| x.prove(context.descend())),
|
||||
Body::And(x) =>
|
||||
{
|
||||
if x.len() == 1
|
||||
{
|
||||
x[0].prove(context.descend(), constraints)
|
||||
}
|
||||
else
|
||||
{
|
||||
let last = x.last().unwrap();
|
||||
let first = Body::And(Vec::from(&x[..(x.len() - 1)]));
|
||||
let mut prover = first.prove_in_module(context.module, constraints.clone());
|
||||
while let Some(new_constraints) = prover.prove()
|
||||
{
|
||||
last.clone().prove(context.descend(), &new_constraints);
|
||||
}
|
||||
}
|
||||
}
|
||||
Body::Or(x) => x.iter().for_each(|x| {
|
||||
info!(target: "Proving", "{}", self);
|
||||
x.prove(context.descend())
|
||||
x.prove(context.descend(), constraints)
|
||||
}),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn substitute(&mut self, constraint: &Constraint)
|
||||
pub fn substitute(&mut self, constraints: &Constraints)
|
||||
{
|
||||
match self
|
||||
{
|
||||
Body::Term(predicate) => predicate.substitute(constraint),
|
||||
Body::And(items) => items.iter_mut().for_each(|x| x.substitute(constraint)),
|
||||
Body::Or(items) => items.iter_mut().for_each(|x| x.substitute(constraint)),
|
||||
Body::Term(predicate) => predicate.substitute(constraints),
|
||||
Body::And(items) => items.iter_mut().for_each(|x| x.substitute(constraints)),
|
||||
Body::Or(items) => items.iter_mut().for_each(|x| x.substitute(constraints)),
|
||||
}
|
||||
}
|
||||
|
||||
@ -129,28 +166,40 @@ impl Body
|
||||
|
||||
impl Predicate
|
||||
{
|
||||
fn prove_with_clause(&self, clause: &Clause, context: Context<'_, '_>)
|
||||
fn prove_with_clause(
|
||||
&self,
|
||||
clause: &Clause,
|
||||
context: Context<'_, '_>,
|
||||
constraints: &Constraints,
|
||||
)
|
||||
{
|
||||
info!(target: "With", "{}", clause);
|
||||
if let Some(constraints) = self.unify(&clause.head)
|
||||
if let Some(unification_constraints) = self.unify(&clause.head)
|
||||
{
|
||||
for x in constraints.iter()
|
||||
let new_constraints = if let Some(c) = unification_constraints.merged(constraints)
|
||||
{
|
||||
info!(target: "Constraints", "{}", x);
|
||||
c
|
||||
}
|
||||
else
|
||||
{
|
||||
info!(target: "Contradiction", "backtracking");
|
||||
return; // Contradiction, backtrack
|
||||
};
|
||||
|
||||
info!(target: "Constraints", "{}", new_constraints);
|
||||
|
||||
match &clause.body
|
||||
{
|
||||
Some(body) =>
|
||||
{
|
||||
let mut next = body.clone();
|
||||
constraints.iter().for_each(|x| next.substitute(x));
|
||||
next.prove(context.descend())
|
||||
next.substitute(constraints);
|
||||
next.prove(context.descend(), &new_constraints)
|
||||
}
|
||||
None =>
|
||||
{
|
||||
info!(target: "[Solution]", "true.");
|
||||
context.yielder.suspend(constraints);
|
||||
context.yielder.suspend(new_constraints.clone());
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -160,42 +209,40 @@ impl Predicate
|
||||
}
|
||||
}
|
||||
|
||||
pub fn unify(&self, other: &Predicate) -> Option<Vec<Constraint>>
|
||||
pub fn unify(&self, other: &Predicate) -> Option<Constraints>
|
||||
{
|
||||
match self
|
||||
{
|
||||
Predicate::Variable(variable) => Some(vec![Constraint {
|
||||
variable: variable.clone(),
|
||||
predicate: other.clone(),
|
||||
}]),
|
||||
Predicate::Variable(variable) =>
|
||||
{
|
||||
let mut c = Constraints::new();
|
||||
c.append(variable.clone(), other.clone());
|
||||
Some(c)
|
||||
}
|
||||
Predicate::Fixed(name, predicates) => match other
|
||||
{
|
||||
Predicate::Variable(variable) => Some(vec![Constraint {
|
||||
variable: variable.clone(),
|
||||
predicate: self.clone(),
|
||||
}]),
|
||||
Predicate::Variable(variable) =>
|
||||
{
|
||||
let mut c = Constraints::new();
|
||||
c.append(variable.clone(), self.clone());
|
||||
Some(c)
|
||||
}
|
||||
Predicate::Fixed(other_name, other_predicates)
|
||||
if other_name == name && predicates.len() == other_predicates.len() =>
|
||||
{
|
||||
if predicates.is_empty()
|
||||
{
|
||||
Some(vec![])
|
||||
Some(Constraints::new())
|
||||
}
|
||||
else
|
||||
{
|
||||
let mut new_constraints = vec![];
|
||||
let mut new_constraints = Constraints::new();
|
||||
for (a, b) in predicates.iter().zip(other_predicates)
|
||||
{
|
||||
if let Some(constraints) = a.unify(b)
|
||||
if let Some(constraints) = b.unify(a)
|
||||
&& let Some(merged) = constraints.merged(&new_constraints)
|
||||
{
|
||||
for c in constraints.iter()
|
||||
{
|
||||
if c.merge_into(&mut new_constraints).is_none()
|
||||
{
|
||||
warn!(target: "Contradiction", "The property is contradictory.");
|
||||
return None;
|
||||
}
|
||||
}
|
||||
new_constraints = merged;
|
||||
}
|
||||
else
|
||||
{
|
||||
@ -210,19 +257,35 @@ impl Predicate
|
||||
}
|
||||
}
|
||||
|
||||
pub fn substitute(&mut self, constraint: &Constraint)
|
||||
pub fn substitute(&mut self, constraints: &Constraints)
|
||||
{
|
||||
match self
|
||||
{
|
||||
Predicate::Variable(name) if *name == constraint.variable =>
|
||||
Predicate::Variable(name) =>
|
||||
{
|
||||
*self = constraint.predicate.clone()
|
||||
}
|
||||
Predicate::Variable(_) => (),
|
||||
Predicate::Fixed(_, predicates) =>
|
||||
{
|
||||
predicates.iter_mut().for_each(|x| x.substitute(constraint))
|
||||
if let Some(predicate) = constraints.set.get(name)
|
||||
{
|
||||
let mut predicate = predicate.clone();
|
||||
predicate.substitute(constraints);
|
||||
*self = predicate;
|
||||
}
|
||||
}
|
||||
Predicate::Fixed(_, predicates) => predicates
|
||||
.iter_mut()
|
||||
.for_each(|x| x.substitute(constraints)),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn contains_variable(&self, variable: &String) -> bool
|
||||
{
|
||||
match self
|
||||
{
|
||||
Predicate::Variable(name) => name == variable,
|
||||
Predicate::Fixed(_, predicates) => predicates
|
||||
.iter()
|
||||
.map(|x| x.contains_variable(variable))
|
||||
.reduce(|a, b| a || b)
|
||||
.unwrap_or(false),
|
||||
}
|
||||
}
|
||||
|
||||
@ -276,33 +339,108 @@ impl Clause
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Constraint
|
||||
impl Constraints
|
||||
{
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
|
||||
pub fn new() -> Self
|
||||
{
|
||||
write!(f, "{} = {}", self.variable, self.predicate)
|
||||
Constraints {
|
||||
set: HashMap::new(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Constraint
|
||||
{
|
||||
fn merge_into(&self, constraints: &mut Vec<Constraint>) -> Option<()>
|
||||
pub fn simplified(&self) -> Constraints
|
||||
{
|
||||
// Check if constraint is contradictory with other constraints
|
||||
for c in constraints.iter()
|
||||
// Perform max substitution
|
||||
let mut new_set = Constraints::new();
|
||||
for (var, predicate) in self.set.iter()
|
||||
{
|
||||
if self.variable == c.variable
|
||||
let mut simpler = predicate.clone();
|
||||
simpler.substitute(self);
|
||||
new_set.set.insert(var.clone(), simpler);
|
||||
}
|
||||
|
||||
// Remove stray variables
|
||||
let mut cleaned_set = new_set.clone();
|
||||
'outer: for (var, _) in new_set.set.iter()
|
||||
{
|
||||
if var.chars().next().is_some_and(|x| x == '_')
|
||||
{
|
||||
let unification = self.predicate.unify(&c.predicate);
|
||||
if unification.is_none()
|
||||
for (_, pred) in new_set.set.iter()
|
||||
{
|
||||
info!(target: "Constraint", "Contradiction. Abort");
|
||||
return None;
|
||||
if pred.contains_variable(var)
|
||||
{
|
||||
continue 'outer;
|
||||
}
|
||||
cleaned_set.set.remove(var);
|
||||
}
|
||||
}
|
||||
}
|
||||
cleaned_set
|
||||
}
|
||||
|
||||
constraints.push(self.clone());
|
||||
Some(())
|
||||
pub fn merged(&self, constraints: &Constraints) -> Option<Constraints>
|
||||
{
|
||||
let mut new = self.clone();
|
||||
for (var, pred) in constraints.set.iter()
|
||||
{
|
||||
if !new.append(var.clone(), pred.clone())
|
||||
{
|
||||
return None;
|
||||
};
|
||||
}
|
||||
Some(new)
|
||||
}
|
||||
|
||||
pub fn append(&mut self, variable: String, predicate: Predicate) -> bool
|
||||
{
|
||||
if let Some(constraint) = self.set.get(&variable)
|
||||
{
|
||||
if let Some(constraints) = predicate.unify(constraint)
|
||||
{
|
||||
if let Some(new) = self.merged(&constraints)
|
||||
{
|
||||
*self = new;
|
||||
true
|
||||
}
|
||||
else
|
||||
{
|
||||
false
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
false
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
self.set.insert(variable, predicate);
|
||||
true
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Default for Constraints
|
||||
{
|
||||
fn default() -> Self
|
||||
{
|
||||
Self::new()
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Constraints
|
||||
{
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
|
||||
{
|
||||
let len = self.set.len();
|
||||
for (i, (variable, predicate)) in self.set.iter().enumerate()
|
||||
{
|
||||
write!(f, "{} = {}", variable, predicate)?;
|
||||
if i != len - 1
|
||||
{
|
||||
write!(f, ", ")?;
|
||||
}
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user