patrick/anthem-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Count program and integer variable IDs separately

Browse Source
This commit is contained in:
Patrick Lühne 2020-02-05 18:50:48 +01:00
parent cd7129a3fa
commit 844f81f5b5
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 17 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/translate/verify_properties.rs
View File

@ -163,7 +163,8 @@ where
.map(|x| (std::rc::Rc::clone(x), completed_definition(x))); .map(|x| (std::rc::Rc::clone(x), completed_definition(x)));
// Earlier log messages may have assigned IDs to the variable declarations, so reset them // Earlier log messages may have assigned IDs to the variable declarations, so reset them
context.variable_declaration_ids.borrow_mut().clear(); context.program_variable_declaration_ids.borrow_mut().clear();
context.integer_variable_declaration_ids.borrow_mut().clear();
let print_title = |title, section_separator| let print_title = |title, section_separator|
{ {

18
src/translate/verify_properties/context.rs
View File

@ -26,7 +26,8 @@ pub(crate) struct Context
pub predicate_declarations: std::cell::RefCell<foliage::PredicateDeclarations>, pub predicate_declarations: std::cell::RefCell<foliage::PredicateDeclarations>,
pub variable_declaration_stack: std::cell::RefCell<crate::VariableDeclarationStack>, pub variable_declaration_stack: std::cell::RefCell<crate::VariableDeclarationStack>,
pub variable_declaration_domains: std::cell::RefCell<VariableDeclarationDomains>, pub variable_declaration_domains: std::cell::RefCell<VariableDeclarationDomains>,
pub variable_declaration_ids: std::cell::RefCell<VariableDeclarationIDs>, pub program_variable_declaration_ids: std::cell::RefCell<VariableDeclarationIDs>,
pub integer_variable_declaration_ids: std::cell::RefCell<VariableDeclarationIDs>,
} }
impl Context impl Context
@ -49,7 +50,10 @@ impl Context
std::cell::RefCell::new(crate::VariableDeclarationStack::new()), std::cell::RefCell::new(crate::VariableDeclarationStack::new()),
variable_declaration_domains: variable_declaration_domains:
std::cell::RefCell::new(VariableDeclarationDomains::new()), std::cell::RefCell::new(VariableDeclarationDomains::new()),
variable_declaration_ids: std::cell::RefCell::new(VariableDeclarationIDs::new()), program_variable_declaration_ids:
std::cell::RefCell::new(VariableDeclarationIDs::new()),
integer_variable_declaration_ids:
std::cell::RefCell::new(VariableDeclarationIDs::new()),
} }
} }
} }
@ -181,7 +185,15 @@ impl crate::traits::VariableDeclarationID for Context
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>) variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
-> usize -> usize
{ {
let mut variable_declaration_ids = self.variable_declaration_ids.borrow_mut(); use crate::traits::VariableDeclarationDomain;
let mut variable_declaration_ids = match self.variable_declaration_domain(
variable_declaration)
{
Some(crate::Domain::Program) => self.program_variable_declaration_ids.borrow_mut(),
Some(crate::Domain::Integer) => self.integer_variable_declaration_ids.borrow_mut(),
None => panic!("all variables should be declared at this point"),
};
match variable_declaration_ids.get(variable_declaration) match variable_declaration_ids.get(variable_declaration)
{ {