From f6f423e30788809af89f219e250108216e361ef6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Wed, 5 Feb 2020 20:19:22 +0100 Subject: [PATCH] Add axioms for order of symbolic constants --- src/translate/verify_properties.rs | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index c0e5730..f3f8c84 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -175,6 +175,7 @@ where let predicate_declarations = context.predicate_declarations.borrow(); let function_declarations = context.function_declarations.borrow(); + let input_constant_declaration_domains = context.input_constant_declaration_domains.borrow(); let completed_definitions = predicate_declarations.iter() // Don’t perform completion for any input predicate .filter(|x| !context.input_predicate_declarations.borrow().contains(*x)) @@ -246,6 +247,33 @@ where &context)); } } + + let symbolic_constants = function_declarations.iter().filter( + |x| !input_constant_declaration_domains.contains_key(*x)); + + let mut last_symbolic_constant: Option> = None; + + for (i, symbolic_constant) in symbolic_constants.enumerate() + { + // Order axioms are only necessary with two or more symbolic constants + if i == 1 + { + println!("% axioms for order of symbolic constants") + } + + if symbolic_constant.arity > 0 + { + return Err(crate::Error::new_logic("unexpected n-ary function declaration")); + } + + if let Some(last_symbolic_constant) = last_symbolic_constant + { + println!("tff(symbolic_constant_order, axiom, p__less__({}, {})).", + last_symbolic_constant.name, symbolic_constant.name); + } + + last_symbolic_constant = Some(std::rc::Rc::clone(symbolic_constant)); + } } for (i, (predicate_declaration, completed_definition)) in completed_definitions.enumerate()