9 Commits

Author SHA1 Message Date
Mark Thom
24e5e39c28 add order preserving tidy_trail, fix random_labeling/2 2019-10-19 00:29:50 -06:00
Mark Thom
ab9a14cc6a add randomness predicates, small but consequential changes to TrailRef 2019-10-17 00:21:21 -06:00
Mark Thom
a641822a1b Merge pull request #206 from triska/master
weighted_maximum/3 now works
2019-10-16 16:17:05 -03:00
Markus Triska
145fee0d36 weighted_maximum/3 now works 2019-10-16 19:18:38 +02:00
Markus Triska
567af2648c support must_be(var, ...) 2019-10-16 19:18:38 +02:00
Mark Thom
42a3bdc357 eliminate lingering attribute goals 2019-10-16 11:38:33 -03:00
Mark Thom
b6a2e26a4f bump toml version number to package clpb on crates 2019-10-16 09:59:41 -03:00
Mark Thom
1557e4705a Merge pull request #204 from triska/master
ADDED: CLP(B), Constraint Logic Programming over Boolean Variables
2019-10-16 02:45:21 -03:00
Markus Triska
ee32e49528 ADDED: CLP(B), Constraint Logic Programming over Boolean Variables
library(clpb) provides CLP(B), Constraint Logic Programming over
Boolean variables. It is a SAT solver that seamlessly integrates into
Prolog in the sense that logic variables are used to state constraints
and report solutions. This library can be used to model and solve many
combinatorial problems such as verification, allocation and covering
tasks.

CLP(B) is an instance of the general CLP(X) scheme, extending logic
programming with reasoning over specialised domains.

The implementation is based on reduced and ordered Binary Decision
Diagrams (BDDs).

Usage examples of this library are available in a public git
repository:

    https://github.com/triska/clpb

For more information, benchmarks and publications visit:

    https://www.metalevel.at/clpb/

The interface of this library is consciously kept compatible with the
CLP(B) solver of SICStus Prolog, which served as the main inspiration
of this library. Many thanks to Mats Carlsson for his elegant example!

It is my hope that library(clpb) will allow a port of cTI, and —
eventually — of Ulrich Neumerkel's GUPU to Scryer Prolog.

                         Boolean expressions
                         ===================

A Boolean expression is one of:

     0                 false
     1                 true
     variable          unknown truth value
     atom              universally quantified variable
     ~ Expr            logical NOT
     Expr + Expr       logical OR
     Expr * Expr       logical AND
     Expr # Expr       exclusive OR
     Var ^ Expr        existential quantification
     Expr =:= Expr     equality
     Expr =\= Expr     disequality (same as #)
     Expr =< Expr      less or equal (implication)
     Expr >= Expr      greater or equal
     Expr < Expr       less than
     Expr > Expr       greater than
     card(Is,Exprs)    see below
     +(Exprs)          see below
     *(Exprs)          see below

where Expr again denotes a Boolean expression.

The Boolean expression card(Is,Exprs) is true iff the number of true
expressions in the list Exprs is a member of the list Is of
integers and integer ranges of the form From-To.

+(Exprs) and *(Exprs) denote, respectively, the disjunction and
conjunction of all elements in the list Exprs of Boolean
expressions.

Atoms denote parametric values that are universally quantified. All
universal quantifiers appear implicitly in front of the entire
expression. In residual goals, universally quantified variables always
appear on the right-hand side of equations. Therefore, they can be
used to express functional dependencies on input variables.

                         Interface predicates
                         ====================

The most frequently used CLP(B) predicates are:

    * sat(+Expr)
      True iff the Boolean expression Expr is satisfiable.

    * taut(+Expr, -T)
      If Expr is a tautology with respect to the posted constraints, succeeds
      with T = 1. If Expr cannot be satisfied, succeeds with T = 0.
      Otherwise, it fails.

    * labeling(+Vs)
      Assigns truth values to the variables Vs such that all constraints
      are satisfied.

The unification of a CLP(B) variable X with a term T is equivalent
to posting the constraint sat(X=:=T).

                               Examples
                               ========

Here is an example session with a few queries and their answers:

    ?- use_module(library(clpb)).
    true.

    ?- sat(X*Y).
    X = Y, Y = 1.

    ?- sat(X * ~X).
    false.

    ?- taut(X * ~X, T).
    T = 0,
    sat(X=:=X).

    ?- sat(X^Y^(X+Y)).
    sat(X=:=X),
    sat(Y=:=Y).

    ?- sat(X*Y + X*Z), labeling([X,Y,Z]).
    X = Z, Z = 1, Y = 0 ;
    X = Y, Y = 1, Z = 0 ;
    X = Y, Y = Z, Z = 1.

    ?- sat(X =< Y), sat(Y =< Z), taut(X =< Z, T).
    T = 1,
    sat(X=:=X*Y),
    sat(Y=:=Y*Z).

    ?- sat(1#X#a#b).
    sat(X=:=a#b).

The pending residual goals constrain remaining variables to Boolean
expressions and are declaratively equivalent to the original query.
The last example illustrates that when applicable, remaining variables
are expressed as functions of universally quantified variables.

                            Obtaining BDDs
                            ==============

By default, CLP(B) residual goals appear in (approximately) algebraic
normal form (ANF). This projection is often computationally expensive.

Assert the fact clpb:clpb_residuals(bdd) to see the BDD representation
of all constraints. This results in faster projection to residual
goals, and is also useful for learning more about BDDs.

For example:

    ?- asserta(clpb:clpb_residuals(bdd)).
    true.

    ?- sat(X#Y).
    node(3)- (v(X, 0)->node(2);node(1)),
    node(1)- (v(Y, 1)->true;false),
    node(2)- (v(Y, 1)->false;true).

Note that this representation cannot be pasted back on the toplevel,
and its details are subject to change. Use copy_term/3 to obtain
such answers as Prolog terms.

The variable order of the BDD is determined by the order in which the
variables first appear in constraints. To obtain different orders,
you can for example use:

    ?- sat(+[1,Y,X]), sat(X#Y).
    node(3)- (v(Y, 0)->node(2);node(1)),
    node(1)- (v(X, 1)->true;false),
    node(2)- (v(X, 1)->false;true).

                           Monotonic CLP(B)
                           ================

In the default execution mode, CLP(B) constraints are not monotonic.
This means that adding constraints can yield new solutions. For
example:

    ?-          sat(X=:=1), X = 1+0.
    false.

    ?- X = 1+0, sat(X=:=1), X = 1+0.
    X = 1+0.

This behaviour is highly problematic from a logical point of view, and
it may render declarative debugging techniques inapplicable (see
https://www.metalevel.at/prolog/debugging for more information).

Assert the fact clpb:monotonic to make CLP(B) monotonic. If this
mode is enabled, then you must wrap CLP(B) variables with the functor
v/1. For example:

    ?- asserta(clpb:monotonic).
    true.

    ?- sat(v(X)=:=1#1).
    X = 0.

Enjoy!
2019-10-16 06:57:43 +02:00
13 changed files with 1999 additions and 111 deletions

View File

@@ -1,6 +1,6 @@
[package] [package]
name = "scryer-prolog" name = "scryer-prolog"
version = "0.8.110" version = "0.8.114"
authors = ["Mark Thom <markjordanthom@gmail.com>"] authors = ["Mark Thom <markjordanthom@gmail.com>"]
build = "build.rs" build = "build.rs"
repository = "https://github.com/mthom/scryer-prolog" repository = "https://github.com/mthom/scryer-prolog"

View File

@@ -2,6 +2,7 @@ use prolog_parser::ast::*;
use crate::prolog::forms::Number; use crate::prolog::forms::Number;
use crate::prolog::machine::machine_indices::*; use crate::prolog::machine::machine_indices::*;
use crate::prolog::rug::rand::RandState;
use ref_thread_local::RefThreadLocal; use ref_thread_local::RefThreadLocal;
@@ -81,6 +82,10 @@ pub enum InlinedClauseType {
IsVar(RegType), IsVar(RegType),
} }
ref_thread_local! {
pub static managed RANDOM_STATE: RandState<'static> = RandState::new();
}
ref_thread_local! { ref_thread_local! {
pub static managed CLAUSE_TYPE_FORMS: BTreeMap<(&'static str, usize), ClauseType> = { pub static managed CLAUSE_TYPE_FORMS: BTreeMap<(&'static str, usize), ClauseType> = {
let mut m = BTreeMap::new(); let mut m = BTreeMap::new();
@@ -223,12 +228,14 @@ pub enum SystemClauseType {
GetCutPoint, GetCutPoint,
GetDoubleQuotes, GetDoubleQuotes,
InstallNewBlock, InstallNewBlock,
Maybe,
ResetBlock, ResetBlock,
ReturnFromAttributeGoals, ReturnFromAttributeGoals,
ReturnFromVerifyAttr, ReturnFromVerifyAttr,
SetBall, SetBall,
SetCutPointByDefault(RegType), SetCutPointByDefault(RegType),
SetDoubleQuotes, SetDoubleQuotes,
SetSeed,
SkipMaxList, SkipMaxList,
Succeed, Succeed,
TermVariables, TermVariables,
@@ -319,6 +326,7 @@ impl SystemClauseType {
clause_name!("$install_inference_counter") clause_name!("$install_inference_counter")
} }
&SystemClauseType::LiftedHeapLength => clause_name!("$lh_length"), &SystemClauseType::LiftedHeapLength => clause_name!("$lh_length"),
&SystemClauseType::Maybe => clause_name!("maybe"),
&SystemClauseType::ModuleHeadIsDynamic => clause_name!("$module_head_is_dynamic"), &SystemClauseType::ModuleHeadIsDynamic => clause_name!("$module_head_is_dynamic"),
&SystemClauseType::ModuleOf => clause_name!("$module_of"), &SystemClauseType::ModuleOf => clause_name!("$module_of"),
&SystemClauseType::NoSuchPredicate => clause_name!("$no_such_predicate"), &SystemClauseType::NoSuchPredicate => clause_name!("$no_such_predicate"),
@@ -329,6 +337,7 @@ impl SystemClauseType {
&SystemClauseType::RemoveInferenceCounter => clause_name!("$remove_inference_counter"), &SystemClauseType::RemoveInferenceCounter => clause_name!("$remove_inference_counter"),
&SystemClauseType::RestoreCutPolicy => clause_name!("$restore_cut_policy"), &SystemClauseType::RestoreCutPolicy => clause_name!("$restore_cut_policy"),
&SystemClauseType::SetCutPoint(_) => clause_name!("$set_cp"), &SystemClauseType::SetCutPoint(_) => clause_name!("$set_cp"),
&SystemClauseType::SetSeed => clause_name!("$set_seed"),
&SystemClauseType::StoreGlobalVar => clause_name!("$store_global_var"), &SystemClauseType::StoreGlobalVar => clause_name!("$store_global_var"),
&SystemClauseType::StoreGlobalVarWithOffset => { &SystemClauseType::StoreGlobalVarWithOffset => {
clause_name!("$store_global_var_with_offset") clause_name!("$store_global_var_with_offset")
@@ -417,6 +426,7 @@ impl SystemClauseType {
("$install_scc_cleaner", 2) => Some(SystemClauseType::InstallSCCCleaner), ("$install_scc_cleaner", 2) => Some(SystemClauseType::InstallSCCCleaner),
("$install_inference_counter", 3) => Some(SystemClauseType::InstallInferenceCounter), ("$install_inference_counter", 3) => Some(SystemClauseType::InstallInferenceCounter),
("$lh_length", 1) => Some(SystemClauseType::LiftedHeapLength), ("$lh_length", 1) => Some(SystemClauseType::LiftedHeapLength),
("$maybe", 0) => Some(SystemClauseType::Maybe),
("$module_of", 2) => Some(SystemClauseType::ModuleOf), ("$module_of", 2) => Some(SystemClauseType::ModuleOf),
("$module_retract_clause", 5) => Some(SystemClauseType::ModuleRetractClause), ("$module_retract_clause", 5) => Some(SystemClauseType::ModuleRetractClause),
("$module_head_is_dynamic", 2) => Some(SystemClauseType::ModuleHeadIsDynamic), ("$module_head_is_dynamic", 2) => Some(SystemClauseType::ModuleHeadIsDynamic),
@@ -450,6 +460,7 @@ impl SystemClauseType {
("$set_ball", 1) => Some(SystemClauseType::SetBall), ("$set_ball", 1) => Some(SystemClauseType::SetBall),
("$set_cp_by_default", 1) => Some(SystemClauseType::SetCutPointByDefault(temp_v!(1))), ("$set_cp_by_default", 1) => Some(SystemClauseType::SetCutPointByDefault(temp_v!(1))),
("$set_double_quotes", 1) => Some(SystemClauseType::SetDoubleQuotes), ("$set_double_quotes", 1) => Some(SystemClauseType::SetDoubleQuotes),
("$set_seed", 1) => Some(SystemClauseType::SetSeed),
("$skip_max_list", 4) => Some(SystemClauseType::SkipMaxList), ("$skip_max_list", 4) => Some(SystemClauseType::SkipMaxList),
("$store_global_var", 2) => Some(SystemClauseType::StoreGlobalVar), ("$store_global_var", 2) => Some(SystemClauseType::StoreGlobalVar),
("$store_global_var_with_offset", 2) => Some(SystemClauseType::StoreGlobalVarWithOffset), ("$store_global_var_with_offset", 2) => Some(SystemClauseType::StoreGlobalVarWithOffset),

View File

@@ -191,7 +191,7 @@ impl<'a> VariableFixtures<'a> {
for term_ref in iter { for term_ref in iter {
if let &TermRef::Var(lvl, cell, ref var) = &term_ref { if let &TermRef::Var(lvl, cell, ref var) = &term_ref {
let mut status = self.perm_vars.remove(var).unwrap_or(( let mut status = self.perm_vars.swap_remove(var).unwrap_or((
VarStatus::Temp(chunk_num, TempVarData::new(lt_arity)), VarStatus::Temp(chunk_num, TempVarData::new(lt_arity)),
Vec::new(), Vec::new(),
)); ));

View File

@@ -20,7 +20,7 @@
'$default_attr_list'([PG | PGs], Module, AttrVar) --> '$default_attr_list'([PG | PGs], Module, AttrVar) -->
( { '$module_of'(Module, PG) } -> [Module:put_atts(AttrVar, PG)] ( { '$module_of'(Module, PG) } -> [Module:put_atts(AttrVar, PG)]
; true ; { true }
), ),
'$default_attr_list'(PGs, Module, AttrVar). '$default_attr_list'(PGs, Module, AttrVar).
'$default_attr_list'([], _, _) --> []. '$default_attr_list'([], _, _) --> [].

1777
src/prolog/lib/clpb.pl Normal file

File diff suppressed because it is too large Load Diff

View File

@@ -33,6 +33,10 @@ must_be(Type, Term) :-
must_be_(Type, _) :- must_be_(Type, _) :-
var(Type), var(Type),
instantiation_error(Type). instantiation_error(Type).
must_be_(var, Term) :-
( var(Term) -> true
; throw(error(uninstantiation_error, _))
).
must_be_(integer, Term) :- check_(integer, integer, Term). must_be_(integer, Term) :- check_(integer, integer, Term).
must_be_(atom, Term) :- check_(atom, atom, Term). must_be_(atom, Term) :- check_(atom, atom, Term).
must_be_(list, Term) :- check_(ilist, list, Term). must_be_(list, Term) :- check_(ilist, list, Term).
@@ -52,6 +56,7 @@ type(type).
type(integer). type(integer).
type(atom). type(atom).
type(list). type(list).
type(var).
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
can_be(Type, Term) can_be(Type, Term)

View File

@@ -4,8 +4,8 @@
%% ?- use_module(library(non_iso)). %% ?- use_module(library(non_iso)).
:- module(non_iso, [bb_b_put/2, bb_get/2, bb_put/2, call_cleanup/2, :- module(non_iso, [bb_b_put/2, bb_get/2, bb_put/2, call_cleanup/2,
call_with_inference_limit/3, forall/2, call_with_inference_limit/3, forall/2, maybe/0,
setup_call_cleanup/3, variant/2]). set_random/1, setup_call_cleanup/3, variant/2]).
forall(Generate, Test) :- forall(Generate, Test) :-
\+ (Generate, \+ Test). \+ (Generate, \+ Test).
@@ -125,3 +125,17 @@ call_with_inference_limit(_, _, R, Bb, B) :-
'$call_with_default_policy'(handle_ile(B, Ball, R)). '$call_with_default_policy'(handle_ile(B, Ball, R)).
variant(X, Y) :- '$variant'(X, Y). variant(X, Y) :- '$variant'(X, Y).
% succeeds with probability 0.5.
maybe :- '$maybe'.
set_random(Seed) :-
( nonvar(Seed) ->
( Seed = seed(S) ->
( var(S) -> throw(error(instantiation_error, set_random/1))
; integer(S) -> '$set_seed'(S)
; throw(error(type_error(integer(S), set_random/1)))
)
)
; throw(error(instantiation_error, set_random/1))
).

View File

@@ -25,6 +25,7 @@ verify_attrs([], _, _, []).
call_verify_attributes(Attrs, _, _, []) :- call_verify_attributes(Attrs, _, _, []) :-
var(Attrs), !. var(Attrs), !.
call_verify_attributes([], _, _, []).
call_verify_attributes([Attr|Attrs], Var, Value, ListOfGoalLists) :- call_verify_attributes([Attr|Attrs], Var, Value, ListOfGoalLists) :-
gather_modules([Attr|Attrs], Modules0), gather_modules([Attr|Attrs], Modules0),
sort(Modules0, Modules), sort(Modules0, Modules),

View File

@@ -14,6 +14,7 @@ pub(super) struct AttrVarInitializer {
pub(super) attr_var_queue: Vec<usize>, pub(super) attr_var_queue: Vec<usize>,
pub(super) bindings: Bindings, pub(super) bindings: Bindings,
pub(super) cp: LocalCodePtr, pub(super) cp: LocalCodePtr,
pub(super) instigating_p: LocalCodePtr,
pub(super) verify_attrs_loc: usize, pub(super) verify_attrs_loc: usize,
pub(super) project_attrs_loc: usize, pub(super) project_attrs_loc: usize,
} }
@@ -24,6 +25,7 @@ impl AttrVarInitializer {
attribute_goals: vec![], attribute_goals: vec![],
attr_var_queue: vec![], attr_var_queue: vec![],
bindings: vec![], bindings: vec![],
instigating_p: LocalCodePtr::default(),
cp: LocalCodePtr::default(), cp: LocalCodePtr::default(),
verify_attrs_loc, verify_attrs_loc,
project_attrs_loc, project_attrs_loc,
@@ -34,16 +36,19 @@ impl AttrVarInitializer {
pub(super) fn reset(&mut self) { pub(super) fn reset(&mut self) {
self.attr_var_queue.clear(); self.attr_var_queue.clear();
self.bindings.clear(); self.bindings.clear();
self.attribute_goals.clear();
} }
} }
impl MachineState { impl MachineState {
pub(super) fn push_attr_var_binding(&mut self, h: usize, addr: Addr) { pub(super) fn push_attr_var_binding(&mut self, h: usize, addr: Addr) {
if self.attr_var_init.bindings.is_empty() { if self.attr_var_init.bindings.is_empty() {
self.attr_var_init.instigating_p = self.p.local();
if self.last_call { if self.last_call {
self.attr_var_init.cp = self.cp; self.attr_var_init.cp = self.cp;
} else { } else {
self.attr_var_init.cp = self.p.local(); self.attr_var_init.cp = self.p.local() + 1;
} }
self.p = CodePtr::VerifyAttrInterrupt(self.attr_var_init.verify_attrs_loc); self.p = CodePtr::VerifyAttrInterrupt(self.attr_var_init.verify_attrs_loc);
@@ -200,7 +205,7 @@ impl Machine {
&mut self.code_repo, &mut self.code_repo,
&mut readline::input_stream(), &mut readline::input_stream(),
); );
self.machine_st self.machine_st
.print_attribute_goals_string(&self.indices.op_dir) .print_attribute_goals_string(&self.indices.op_dir)
} }

View File

@@ -178,10 +178,11 @@ impl From<Ref> for Addr {
} }
} }
#[derive(Clone)] #[derive(Clone, Copy)]
pub enum TrailRef { pub enum TrailRef {
Ref(Ref), Ref(Ref),
AttrVarLink(usize, Addr), AttrVarHeapLink(usize),
AttrVarListLink(usize, usize),
} }
impl From<Ref> for TrailRef { impl From<Ref> for TrailRef {
@@ -468,6 +469,12 @@ pub struct IndexStore {
} }
impl IndexStore { impl IndexStore {
pub fn reset_global_variable_offsets(&mut self) {
for (_, ref mut offset) in self.global_variables.values_mut() {
*offset = None;
}
}
pub fn predicate_exists( pub fn predicate_exists(
&self, &self,
name: ClauseName, name: ClauseName,

View File

@@ -648,9 +648,15 @@ impl MachineState {
self.tr += 1; self.tr += 1;
} }
} }
TrailRef::AttrVarLink(h, prev_addr) => { TrailRef::AttrVarHeapLink(h) => {
if h < self.hb { if h < self.hb {
self.trail.push(TrailRef::AttrVarLink(h, prev_addr)); self.trail.push(TrailRef::AttrVarHeapLink(h));
self.tr += 1;
}
}
TrailRef::AttrVarListLink(h, l) => {
if h < self.hb {
self.trail.push(TrailRef::AttrVarListLink(h, l));
self.tr += 1; self.tr += 1;
} }
} }
@@ -680,7 +686,7 @@ impl MachineState {
// additions, now that deleted attributes can be undeleted by // additions, now that deleted attributes can be undeleted by
// backtracking. // backtracking.
for i in (a1..a2).rev() { for i in (a1..a2).rev() {
match self.trail[i].clone() { match self.trail[i] {
TrailRef::Ref(Ref::HeapCell(h)) => { TrailRef::Ref(Ref::HeapCell(h)) => {
self.heap[h] = HeapCellValue::Addr(Addr::HeapCell(h)) self.heap[h] = HeapCellValue::Addr(Addr::HeapCell(h))
} }
@@ -690,8 +696,11 @@ impl MachineState {
TrailRef::Ref(Ref::StackCell(fr, sc)) => { TrailRef::Ref(Ref::StackCell(fr, sc)) => {
self.and_stack[fr][sc] = Addr::StackCell(fr, sc) self.and_stack[fr][sc] = Addr::StackCell(fr, sc)
} }
TrailRef::AttrVarLink(h, prev_addr) => { TrailRef::AttrVarHeapLink(h) => {
self.heap[h] = HeapCellValue::Addr(prev_addr) self.heap[h] = HeapCellValue::Addr(Addr::HeapCell(h));
}
TrailRef::AttrVarListLink(h, l) => {
self.heap[h] = HeapCellValue::Addr(Addr::Lis(l));
} }
} }
} }
@@ -732,28 +741,21 @@ impl MachineState {
} }
let b = self.b - 1; let b = self.b - 1;
let mut i = self.or_stack[b].tr; let hb = self.hb;
let mut offset = 0;
while i < self.tr { for i in self.or_stack[b].tr .. self.tr {
let tr_i = self.trail[i].clone(); match self.trail[i] {
let hb = self.hb;
match tr_i {
TrailRef::Ref(Ref::AttrVar(tr_i)) TrailRef::Ref(Ref::AttrVar(tr_i))
| TrailRef::Ref(Ref::HeapCell(tr_i)) | TrailRef::Ref(Ref::HeapCell(tr_i))
| TrailRef::AttrVarLink(tr_i, _) => { | TrailRef::AttrVarHeapLink(tr_i)
if tr_i < hb { | TrailRef::AttrVarListLink(tr_i, _) =>
i += 1; if tr_i >= hb {
} else { offset += 1;
let tr = self.tr; } else {
let val = self.trail[tr - 1].clone(); self.trail[i - offset] = self.trail[i];
self.trail[i] = val; },
self.trail.pop();
self.tr -= 1;
}
}
TrailRef::Ref(Ref::StackCell(fr, _)) => { TrailRef::Ref(Ref::StackCell(fr, _)) => {
let b = self.b - 1;
let fr_gi = self.and_stack[fr].global_index; let fr_gi = self.and_stack[fr].global_index;
let b_gi = if !self.or_stack.is_empty() { let b_gi = if !self.or_stack.is_empty() {
self.or_stack[b].global_index self.or_stack[b].global_index
@@ -761,20 +763,19 @@ impl MachineState {
0 0
}; };
if fr_gi < b_gi { if fr_gi >= b_gi {
i += 1; offset += 1;
} else { } else {
let tr = self.tr; self.trail[i - offset] = self.trail[i];
let val = self.trail[tr - 1].clone();
self.trail[i] = val;
self.trail.pop();
self.tr -= 1;
} }
} }
}; }
} }
}
self.tr -= offset;
self.trail.truncate(self.tr);
}
#[inline] #[inline]
fn write_char_to_string(&mut self, s: &mut StringList, c: char) -> bool { fn write_char_to_string(&mut self, s: &mut StringList, c: char) -> bool {
self.pstr_trail(s.clone()); self.pstr_trail(s.clone());
@@ -1665,7 +1666,7 @@ impl MachineState {
} else if s.is_expandable() { } else if s.is_expandable() {
self.heap self.heap
.push(HeapCellValue::Addr(Addr::Con(Constant::String(s.clone())))); .push(HeapCellValue::Addr(Addr::Con(Constant::String(s.clone()))));
self.s = h; self.s = h;
self.mode = MachineMode::Read; self.mode = MachineMode::Read;
} else { } else {
@@ -3424,56 +3425,4 @@ impl MachineState {
self.heap_locs.clear(); self.heap_locs.clear();
self.lifted_heap.clear(); self.lifted_heap.clear();
} }
pub(super) fn sink_to_snapshot(&mut self) -> MachineState {
let mut snapshot = MachineState::with_capacity(0);
snapshot.hb = self.hb;
snapshot.e = self.e;
snapshot.b = self.b;
snapshot.b0 = self.b0;
snapshot.s = self.s;
snapshot.tr = self.tr;
snapshot.pstr_tr = self.pstr_tr;
snapshot.num_of_args = self.num_of_args;
snapshot.fail = self.fail;
snapshot.trail = mem::replace(&mut self.trail, vec![]);
snapshot.pstr_trail = mem::replace(&mut self.pstr_trail, vec![]);
snapshot.heap = self.heap.take();
snapshot.mode = self.mode;
snapshot.and_stack = self.and_stack.take();
snapshot.or_stack = self.or_stack.take();
snapshot.registers = mem::replace(&mut self.registers, vec![]);
snapshot.block = self.block;
snapshot.ball = self.ball.take();
snapshot.lifted_heap = mem::replace(&mut self.lifted_heap, vec![]);
snapshot
}
pub(super) fn absorb_snapshot(&mut self, mut snapshot: MachineState) {
self.hb = snapshot.hb;
self.e = snapshot.e;
self.b = snapshot.b;
self.b0 = snapshot.b0;
self.s = snapshot.s;
self.tr = snapshot.tr;
self.pstr_tr = snapshot.pstr_tr;
self.num_of_args = snapshot.num_of_args;
self.fail = snapshot.fail;
self.trail = mem::replace(&mut snapshot.trail, vec![]);
self.pstr_trail = mem::replace(&mut snapshot.pstr_trail, vec![]);
self.heap = snapshot.heap.take();
self.mode = snapshot.mode;
self.and_stack = snapshot.and_stack.take();
self.or_stack = snapshot.or_stack.take();
self.registers = mem::replace(&mut snapshot.registers, vec![]);
self.block = snapshot.block;
self.ball = snapshot.ball.take();
self.lifted_heap = mem::replace(&mut snapshot.lifted_heap, vec![]);
}
} }

View File

@@ -6,6 +6,7 @@ use crate::prolog::fixtures::*;
use crate::prolog::forms::*; use crate::prolog::forms::*;
use crate::prolog::heap_print::*; use crate::prolog::heap_print::*;
use crate::prolog::instructions::*; use crate::prolog::instructions::*;
use crate::prolog::machine::heap::Heap;
use crate::prolog::read::*; use crate::prolog::read::*;
use crate::prolog::write::{next_keypress, ContinueResult}; use crate::prolog::write::{next_keypress, ContinueResult};
@@ -71,6 +72,7 @@ impl MachinePolicies {
pub struct Machine { pub struct Machine {
pub(super) machine_st: MachineState, pub(super) machine_st: MachineState,
pub(super) inner_heap: Heap,
pub(super) policies: MachinePolicies, pub(super) policies: MachinePolicies,
pub(super) indices: IndexStore, pub(super) indices: IndexStore,
pub(super) code_repo: CodeRepo, pub(super) code_repo: CodeRepo,
@@ -227,13 +229,13 @@ impl Machine {
} }
pub fn run_init_code(&mut self, code: Code) { pub fn run_init_code(&mut self, code: Code) {
let old_machine_st = self.machine_st.sink_to_snapshot(); let old_machine_st = self.sink_to_snapshot();
self.machine_st.reset(); self.machine_st.reset();
self.code_repo.cached_query = code; self.code_repo.cached_query = code;
self.run_query(&AllocVarDict::new()); self.run_query(&AllocVarDict::new());
self.machine_st.absorb_snapshot(old_machine_st); self.absorb_snapshot(old_machine_st);
} }
pub fn run_top_level(&mut self) { pub fn run_top_level(&mut self) {
@@ -260,6 +262,7 @@ impl Machine {
pub fn new(prolog_stream: PrologStream) -> Self { pub fn new(prolog_stream: PrologStream) -> Self {
let mut wam = Machine { let mut wam = Machine {
machine_st: MachineState::new(), machine_st: MachineState::new(),
inner_heap: Heap::with_capacity(256 * 256),
policies: MachinePolicies::new(), policies: MachinePolicies::new(),
indices: IndexStore::new(), indices: IndexStore::new(),
code_repo: CodeRepo::new(), code_repo: CodeRepo::new(),
@@ -570,9 +573,14 @@ impl Machine {
}; };
let stream = parsing_stream(s.as_bytes()); let stream = parsing_stream(s.as_bytes());
let snapshot = self.sink_to_snapshot();
let policies = mem::replace(&mut self.policies, MachinePolicies::new());
let snapshot = self.machine_st.sink_to_snapshot();
self.machine_st.reset(); self.machine_st.reset();
self.machine_st.heap = mem::replace(
&mut self.inner_heap,
Heap::with_capacity(0),
);
let result = match stream_to_toplevel(stream, self) { let result = match stream_to_toplevel(stream, self) {
Ok(packet) => compile_term(self, packet), Ok(packet) => compile_term(self, packet),
@@ -580,6 +588,8 @@ impl Machine {
}; };
self.handle_eval_session(result, snapshot); self.handle_eval_session(result, snapshot);
self.indices.reset_global_variable_offsets();
self.policies = policies;
} }
REPLCodePtr::UseModule => REPLCodePtr::UseModule =>
self.use_module(ModuleSource::Library), self.use_module(ModuleSource::Library),
@@ -594,10 +604,66 @@ impl Machine {
self.machine_st.p = CodePtr::Local(p); self.machine_st.p = CodePtr::Local(p);
} }
fn sink_to_snapshot(&mut self) -> MachineState {
let mut snapshot = MachineState::with_capacity(0);
snapshot.hb = self.machine_st.hb;
snapshot.e = self.machine_st.e;
snapshot.b = self.machine_st.b;
snapshot.b0 = self.machine_st.b0;
snapshot.s = self.machine_st.s;
snapshot.tr = self.machine_st.tr;
snapshot.pstr_tr = self.machine_st.pstr_tr;
snapshot.num_of_args = self.machine_st.num_of_args;
snapshot.fail = self.machine_st.fail;
snapshot.trail = mem::replace(&mut self.machine_st.trail, vec![]);
snapshot.pstr_trail = mem::replace(&mut self.machine_st.pstr_trail, vec![]);
snapshot.heap = self.machine_st.heap.take();
snapshot.mode = self.machine_st.mode;
snapshot.and_stack = self.machine_st.and_stack.take();
snapshot.or_stack = self.machine_st.or_stack.take();
snapshot.registers = mem::replace(&mut self.machine_st.registers, vec![]);
snapshot.block = self.machine_st.block;
snapshot.ball = self.machine_st.ball.take();
snapshot.lifted_heap = mem::replace(&mut self.machine_st.lifted_heap, vec![]);
snapshot
}
fn absorb_snapshot(&mut self, mut snapshot: MachineState) {
self.machine_st.hb = snapshot.hb;
self.machine_st.e = snapshot.e;
self.machine_st.b = snapshot.b;
self.machine_st.b0 = snapshot.b0;
self.machine_st.s = snapshot.s;
self.machine_st.tr = snapshot.tr;
self.machine_st.pstr_tr = snapshot.pstr_tr;
self.machine_st.num_of_args = snapshot.num_of_args;
self.machine_st.fail = snapshot.fail;
self.machine_st.trail = mem::replace(&mut snapshot.trail, vec![]);
self.machine_st.pstr_trail = mem::replace(&mut snapshot.pstr_trail, vec![]);
self.inner_heap = self.machine_st.heap.take();
self.inner_heap.truncate(0);
self.machine_st.heap = snapshot.heap.take();
self.machine_st.mode = snapshot.mode;
self.machine_st.and_stack = snapshot.and_stack.take();
self.machine_st.or_stack = snapshot.or_stack.take();
self.machine_st.registers = mem::replace(&mut snapshot.registers, vec![]);
self.machine_st.block = snapshot.block;
self.machine_st.ball = snapshot.ball.take();
self.machine_st.lifted_heap = mem::replace(&mut snapshot.lifted_heap, vec![]);
}
fn propagate_exception_to_toplevel(&mut self, snapshot: MachineState) { fn propagate_exception_to_toplevel(&mut self, snapshot: MachineState) {
let ball = self.machine_st.ball.take(); let ball = self.machine_st.ball.take();
self.machine_st.absorb_snapshot(snapshot); self.absorb_snapshot(snapshot);
self.machine_st.ball = ball; self.machine_st.ball = ball;
let h = self.machine_st.heap.h; let h = self.machine_st.heap.h;
@@ -617,7 +683,7 @@ impl Machine {
}; };
let attr_goals = self.attribute_goals(); let attr_goals = self.attribute_goals();
if !(self.machine_st.b > 0) { if !(self.machine_st.b > 0) {
if bindings.is_empty() { if bindings.is_empty() {
let space = if requires_space(&attr_goals, ".") { let space = if requires_space(&attr_goals, ".") {
@@ -632,7 +698,7 @@ impl Machine {
println!("true."); println!("true.");
} }
self.machine_st.absorb_snapshot(snapshot); self.absorb_snapshot(snapshot);
return; return;
} }
} else if bindings.is_empty() && attr_goals.is_empty() { } else if bindings.is_empty() && attr_goals.is_empty() {
@@ -664,7 +730,7 @@ impl Machine {
} }
ContinueResult::Conclude => { ContinueResult::Conclude => {
print!(" ...\r\n"); print!(" ...\r\n");
self.machine_st.absorb_snapshot(snapshot); self.absorb_snapshot(snapshot);
return; return;
} }
}; };
@@ -676,12 +742,12 @@ impl Machine {
return; return;
} else { } else {
print!("false.\r\n"); print!("false.\r\n");
self.machine_st.absorb_snapshot(snapshot); self.absorb_snapshot(snapshot);
return; return;
} }
} }
EvalSession::Error(err) => { EvalSession::Error(err) => {
self.machine_st.absorb_snapshot(snapshot); self.absorb_snapshot(snapshot);
self.throw_session_error(err, (clause_name!("repl"), 0)); self.throw_session_error(err, (clause_name!("repl"), 0));
return; return;
} }
@@ -712,7 +778,7 @@ impl Machine {
} }
}, },
EvalSession::Error(err) => { EvalSession::Error(err) => {
self.machine_st.absorb_snapshot(snapshot); self.absorb_snapshot(snapshot);
self.throw_session_error(err, (clause_name!("repl"), 0)); self.throw_session_error(err, (clause_name!("repl"), 0));
return; return;
} }
@@ -725,7 +791,7 @@ impl Machine {
_ => println!("true.") _ => println!("true.")
} }
self.machine_st.absorb_snapshot(snapshot); self.absorb_snapshot(snapshot);
} }
pub(super) fn run_query(&mut self, alloc_locs: &AllocVarDict) { pub(super) fn run_query(&mut self, alloc_locs: &AllocVarDict) {
@@ -1048,7 +1114,13 @@ impl MachineState {
CodePtr::VerifyAttrInterrupt(_) => { CodePtr::VerifyAttrInterrupt(_) => {
self.p = CodePtr::Local(self.attr_var_init.cp); self.p = CodePtr::Local(self.attr_var_init.cp);
if !self.verify_attr_stepper(indices, policies, code_repo, prolog_stream) { let instigating_p = CodePtr::Local(self.attr_var_init.instigating_p);
let instigating_instr = code_repo.lookup_instr(false, &instigating_p).unwrap();
if instigating_instr.as_ref().is_head_instr() {
let cp = self.p.local();
self.run_verify_attr_interrupt(cp);
} else if !self.verify_attr_stepper(indices, policies, code_repo, prolog_stream) {
if self.fail { if self.fail {
break; break;
} }

View File

@@ -17,6 +17,8 @@ use crate::prolog::ordered_float::OrderedFloat;
use crate::prolog::read::{readline, PrologStream}; use crate::prolog::read::{readline, PrologStream};
use crate::prolog::rug::Integer; use crate::prolog::rug::Integer;
use crate::ref_thread_local::RefThreadLocal;
use indexmap::{IndexMap, IndexSet}; use indexmap::{IndexMap, IndexSet};
use std::collections::VecDeque; use std::collections::VecDeque;
@@ -679,7 +681,8 @@ impl MachineState {
let c = self.int_to_char_code(&n, "atom_codes", 2)?; let c = self.int_to_char_code(&n, "atom_codes", 2)?;
chars.push(c as char); chars.push(c as char);
} }
&Addr::Con(Constant::CharCode(c)) => chars.push(c as char), &Addr::Con(Constant::CharCode(c)) =>
chars.push(c as char),
_ => { _ => {
let err = MachineError::type_error( let err = MachineError::type_error(
ValidType::Integer, ValidType::Integer,
@@ -1018,8 +1021,14 @@ impl MachineState {
tail tail
}; };
let trail_ref = match old_addr {
Addr::HeapCell(h) => TrailRef::AttrVarHeapLink(h),
Addr::Lis(l) => TrailRef::AttrVarListLink(l1 + 1, l),
_ => unreachable!()
};
self.heap[l1 + 1] = HeapCellValue::Addr(tail); self.heap[l1 + 1] = HeapCellValue::Addr(tail);
self.trail(TrailRef::AttrVarLink(l1 + 1, old_addr)); self.trail(trail_ref);
} }
} }
} }
@@ -1041,7 +1050,7 @@ impl MachineState {
}; };
self.heap[h + 1] = HeapCellValue::Addr(tail); self.heap[h + 1] = HeapCellValue::Addr(tail);
self.trail(TrailRef::AttrVarLink(h + 1, Addr::Lis(l))); self.trail(TrailRef::AttrVarListLink(h + 1, l));
} }
_ => unreachable!(), _ => unreachable!(),
} }
@@ -1255,6 +1264,19 @@ impl MachineState {
_ => self.fail = true, _ => self.fail = true,
} }
} }
&SystemClauseType::Maybe => {
let result = {
let mut rand = RANDOM_STATE.borrow_mut();
if rand.bits(1) == 0 {
true
} else {
false
}
};
self.fail = result;
}
&SystemClauseType::OpDeclaration => { &SystemClauseType::OpDeclaration => {
let priority = self[temp_v!(1)].clone(); let priority = self[temp_v!(1)].clone();
let specifier = self[temp_v!(2)].clone(); let specifier = self[temp_v!(2)].clone();
@@ -1664,7 +1686,7 @@ impl MachineState {
return Ok(()); return Ok(());
} }
&SystemClauseType::ReturnFromAttributeGoals => { &SystemClauseType::ReturnFromAttributeGoals => {
self.deallocate(); self.deallocate();
self.p = CodePtr::Local(LocalCodePtr::TopLevel(0, 0)); self.p = CodePtr::Local(LocalCodePtr::TopLevel(0, 0));
return Ok(()); return Ok(());
} }
@@ -1834,6 +1856,31 @@ impl MachineState {
} }
&SystemClauseType::SetBall => &SystemClauseType::SetBall =>
self.set_ball(), self.set_ball(),
&SystemClauseType::SetSeed => {
let seed = self.store(self.deref(self[temp_v!(1)].clone()));
let seed = match seed {
Addr::Con(Constant::Integer(n)) =>
n,
Addr::Con(Constant::CharCode(c)) =>
Integer::from(c),
Addr::Con(Constant::Rational(r)) => {
if r.denom() == &1 {
r.numer().clone()
} else {
self.fail = true;
return Ok(());
}
}
_ => {
self.fail = true;
return Ok(());
}
};
let mut rand = RANDOM_STATE.borrow_mut();
rand.seed(&seed);
}
&SystemClauseType::SkipMaxList => &SystemClauseType::SkipMaxList =>
if let Err(err) = self.skip_max_list() { if let Err(err) = self.skip_max_list() {
return Err(err); return Err(err);