Fix for constraints after promoting inputvars #224
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
FYI @zhanghongce, here's the fix I mentioned separately. |
ahmed-irfan
approved these changes
Jan 21, 2021
makaimann
added a commit
that referenced
this pull request
Jan 24, 2021
* Add a functional unroller * WIP on functional unrolling refinement * Fix in functional unroller * More WIP on functional unrolling refinement in ic3sa * Turn off assume-prop in pre-state by default (#219) * Move prop_in_trans implementation to cpp * Change default to not assume property in pre-state * IC3Base: Add option to disable unsat core generalization (#217) * Add option to disable unsatcore generalization in rel_ind_check * Remove unnecessary assertion -- fix_if_intersects_initial doesn't use solver_ for checking sat * Improve help message * Start frame with property in it, as opposed to keeping property in pre-state of trans (#218) * Improve Refinement in cegar values (#221) * rename files * Revert "rename files" This reverts commit 35107ad. * improve refinement in cegar-values * Fix for constraints after promoting inputvars (#224) * default to true for constraints second arg * Re-populate constraints after promoting input variables * Put everything in the pass * Use updated system * Add a simple test for that issue * Use default inductive_generalization for option 0 in mbic3 (#226) * Add constraints to functional unrolling * Fix off-by-one error in last_model_values * Remove unused symbolic post-image Co-authored-by: Ahmed Irfan <[email protected]>
makaimann
added a commit
that referenced
this pull request
Jan 30, 2021
* Add SubTermCollector and basic test for it * Temporarily pull a branch of smt-switch * Pull newer smt-switch * Stub out IC3SA implementation * Add refine method -- abstraction not needed, only in form of clauses * Stub out more methods for ic3sa * set up initial abstraction * First pass get_equivalence_classes_from_model implementation * First pass on get_model_ic3formula for IC3SA * First pass on IC3SA::check_ts * First pass on ic3formula_check_valid in IC3SA * remove TODO * Add test for untiming with FunctionalUnroller * Mark FunctionalUnroller::at_time as override * Don't include ITEs in subterm walker by default * Create method is_predicate * Keep track of predicates in subterm walker * Include predicates in ic3formula model for ic3sa * Stub out intersects_bad in IC3SA * First pass at projection in IC3SA * Add a minor comment * Update IC3SA constructor * Remove old NYI exception * Add some todos * First pass on generalize_predecessor for IC3SA * Add a TODO -- not done with generalize_predecessor * Add helper method for removing ITEs under a given model * Recover CEX trace in IC3SA::refine * Fix copy-paste mistake * WIP on refinement in IC3SA * Take and return vectors in remove_ites_under_model * Partial fix for symbolic_post_image * More WIP on refinement * Finish get_model_ic3formula implementation in ic3sa * Add ic3sa engine option * Minor * minor fix * Add debug printing method * Fix in SubTermCollector * Add a todo * Add include_symbols option to is_predicate * Remove some engines from all_engines for now * Fix: don't want both polarities of a literal in get_predicates * Allow literals and predicates in ic3sa ic3formulas * Add option to show invariant * Don't pass verbosity through to COI in ic3sa * Add another simple sample problem * Allow bvnot for eq_lit * Get rid of is_eq_lit * Fix initial substitute method * Minor fix in construct_partition * Add some todos * WIP on refinement * More work on refinement * More WIP on refine * simplify cex trace traversal * Clear proof goals in refinement * Add size method to ProofGoalQueue * Use local logger in fcoi * Logger message for generalize_predecessor * WIP for removing fresh symbolic constants from axiom in refine * Add only curr terms to abstraction * Add method for promoting an input variable to be a state variable * Fix in promote_inputvar * Promote input variables to state variables * Use fresh unrolling from i-1 * Working for two basic examples * Some cleanup * Handle length-one CEX * Add axiom to trans_label_ assumptions * Use one method for adding to term abstraction * Don't combine terms because btor might simplify * Improvements to term analysis for boolector * Hack fix for ic3formula_check_valid with boolector * Fix in check_valid * Add new sample problem * Update debug printing methods * IC3SA fixes: keep track of representatives and intersects_bad generalization might fail * Fix for cube creation * Minor * Fix for is_predicate * Fix in collect subterms * Minor * Add basic test for IC3SA * Minor fix in subterm collector * Updates to IC3SA for prover interface updates * Other fixes to bring in line with changes * Fixes for changes to master * minor * De-duplicate using a set * Add assertions construct_partition * Rely on is_lit from smt-switch * Ic3sa justify coi (#195) * WIP * WIP on justify_coi * First pass implementation on get_controlling * Use justify_coi -- currently failing * Some fixes in justify_coi * Fix in predicate projection * Fix in justify_coi -- still failing an assertion * Another fix for justify_coi: always visit Ite condition * Compilation fix: don't rely on template deduction * Include constraints in justify_coi * Add Implies and refactor for controlling args * Remove unused variable * format * Compilation fixes for upstream changes * Guard interpolant based engines * Add sample file * Fix in justify coi -- filter variables after traversing whole formula * Temporarily remove assertion * Don't replace ITEs because we don't want to fix a path * Use promote inputvars for ic3sa * Increase verbosity for printing axiom * Ic3sa functional (#220) * Add a functional unroller * WIP on functional unrolling refinement * Fix in functional unroller * More WIP on functional unrolling refinement in ic3sa * Turn off assume-prop in pre-state by default (#219) * Move prop_in_trans implementation to cpp * Change default to not assume property in pre-state * IC3Base: Add option to disable unsat core generalization (#217) * Add option to disable unsatcore generalization in rel_ind_check * Remove unnecessary assertion -- fix_if_intersects_initial doesn't use solver_ for checking sat * Improve help message * Start frame with property in it, as opposed to keeping property in pre-state of trans (#218) * Improve Refinement in cegar values (#221) * rename files * Revert "rename files" This reverts commit 35107ad. * improve refinement in cegar-values * Fix for constraints after promoting inputvars (#224) * default to true for constraints second arg * Re-populate constraints after promoting input variables * Put everything in the pass * Use updated system * Add a simple test for that issue * Use default inductive_generalization for option 0 in mbic3 (#226) * Add constraints to functional unrolling * Fix off-by-one error in last_model_values * Remove unused symbolic post-image Co-authored-by: Ahmed Irfan <[email protected]> * Pop solver context after cex * Add ic3sa to ic3_variants * Get all possible controlling terms * recursive justify_coi * handle constraints in recursive justify_coi * Fixes in IC3SA (#238) Message: This PR adds a fallback procedure for functional refinement. There's an issue where functional refinement can result in a value due to simplification in the smt-solver. In that case, it will fall back to a simpler refinement approach. Additionally, there are cases (especially when using actual input variables that cannot have lemmas learned over them) where functional refinement can add the same lemma again due to simplification. Another branch (ic3sa-fixes) is experimenting with using a logging solver to avoid that. It also makes sure to learn the lemma which is important for making progress. To do this it uses a relation view of the main transition system. It also splits the constraints into the conjunctive partition for a better unsat core. This PR also fixes an assertion failure that would show up occasionally (more often with mathsat) where the predecessor was over-generalized. There were several iterations to fix this including a recursive justify coi implementation (I think the important part is traversing as a tree instead of a DAG because location of the node matters), and various other attempts. In the end, the only thing that worked was adding all variables appearing in constraints (and in the state update of variables from next constraints). These fixes may be overly conservative, but at least they work and can be improved upon in a separate PR. There is good evidence that this assertion failure no longer occurs (several runs with different random seeds don't turn it up). Unfortunately this is highly non-deterministic so I can't be fully sure. There are still some expected errors when using mathsat as the underlying solver. There appears to be a rewriting bug so that when we create an equality that should be guaranteed to be true in the model (because they had the same value) it ends up being a different term (e.g. rewritten to one that evaluates to false). This bug was already reported and there's not much to do now. However, this seems okay because boolector is better for this algorithm anyway. Commits: * deduplicate labels * comment * Fix in test * Add a new test * Add a fallback refinement procedure * Straightforward substitution * Use relational system in IC3SA for learning path constraints * Minor * Learn path axiom * Value substitution with one input unrolled (state var replaced) * Have two refinement options * Add ic3sa to ic3_variants * Get all possible controlling terms * recursive justify_coi * add constraints * Get a reference * Add learned lemma to trans_label_ * Justify coi for all constraints * Justify next constraint and add a comment * Return new terms when updating abstraction and only add symbols from new terms * Just include all variables from constraints * Fix state update lookup * Minor cleanup * Some clean up * Clarification * Remove empty check of input variable sort * Pass equivalence classes by reference to get updated * Address Ahmed's comment Co-authored-by: Ahmed Irfan <[email protected]>
makaimann
added a commit
that referenced
this pull request
Jan 30, 2021
…sects" support (#242) * Add SubTermCollector and basic test for it * Temporarily pull a branch of smt-switch * Pull newer smt-switch * Stub out IC3SA implementation * Add refine method -- abstraction not needed, only in form of clauses * Stub out more methods for ic3sa * set up initial abstraction * First pass get_equivalence_classes_from_model implementation * First pass on get_model_ic3formula for IC3SA * First pass on IC3SA::check_ts * First pass on ic3formula_check_valid in IC3SA * remove TODO * Add test for untiming with FunctionalUnroller * Mark FunctionalUnroller::at_time as override * Don't include ITEs in subterm walker by default * Create method is_predicate * Keep track of predicates in subterm walker * Include predicates in ic3formula model for ic3sa * Stub out intersects_bad in IC3SA * First pass at projection in IC3SA * Add a minor comment * Update IC3SA constructor * Remove old NYI exception * Add some todos * First pass on generalize_predecessor for IC3SA * Add a TODO -- not done with generalize_predecessor * Add helper method for removing ITEs under a given model * Recover CEX trace in IC3SA::refine * Fix copy-paste mistake * WIP on refinement in IC3SA * Take and return vectors in remove_ites_under_model * Partial fix for symbolic_post_image * More WIP on refinement * Finish get_model_ic3formula implementation in ic3sa * Add ic3sa engine option * Minor * minor fix * Add debug printing method * Fix in SubTermCollector * Add a todo * Add include_symbols option to is_predicate * Remove some engines from all_engines for now * Fix: don't want both polarities of a literal in get_predicates * Allow literals and predicates in ic3sa ic3formulas * Add option to show invariant * Don't pass verbosity through to COI in ic3sa * Add another simple sample problem * Allow bvnot for eq_lit * Get rid of is_eq_lit * Fix initial substitute method * Minor fix in construct_partition * Add some todos * WIP on refinement * More work on refinement * More WIP on refine * simplify cex trace traversal * Clear proof goals in refinement * Add size method to ProofGoalQueue * Use local logger in fcoi * Logger message for generalize_predecessor * WIP for removing fresh symbolic constants from axiom in refine * Add only curr terms to abstraction * Add method for promoting an input variable to be a state variable * Fix in promote_inputvar * Promote input variables to state variables * Use fresh unrolling from i-1 * Working for two basic examples * Some cleanup * Handle length-one CEX * Add axiom to trans_label_ assumptions * Use one method for adding to term abstraction * Don't combine terms because btor might simplify * Improvements to term analysis for boolector * Hack fix for ic3formula_check_valid with boolector * Fix in check_valid * Add new sample problem * Update debug printing methods * IC3SA fixes: keep track of representatives and intersects_bad generalization might fail * Fix for cube creation * Minor * Fix for is_predicate * Fix in collect subterms * Minor * Add basic test for IC3SA * Minor fix in subterm collector * Updates to IC3SA for prover interface updates * Other fixes to bring in line with changes * Fixes for changes to master * minor * De-duplicate using a set * Add assertions construct_partition * Rely on is_lit from smt-switch * Ic3sa justify coi (#195) * WIP * WIP on justify_coi * First pass implementation on get_controlling * Use justify_coi -- currently failing * Some fixes in justify_coi * Fix in predicate projection * Fix in justify_coi -- still failing an assertion * Another fix for justify_coi: always visit Ite condition * Compilation fix: don't rely on template deduction * Include constraints in justify_coi * Add Implies and refactor for controlling args * Remove unused variable * format * Compilation fixes for upstream changes * Guard interpolant based engines * Add sample file * Fix in justify coi -- filter variables after traversing whole formula * Temporarily remove assertion * Don't replace ITEs because we don't want to fix a path * Use promote inputvars for ic3sa * Increase verbosity for printing axiom * Ic3sa functional (#220) * Add a functional unroller * WIP on functional unrolling refinement * Fix in functional unroller * More WIP on functional unrolling refinement in ic3sa * Turn off assume-prop in pre-state by default (#219) * Move prop_in_trans implementation to cpp * Change default to not assume property in pre-state * IC3Base: Add option to disable unsat core generalization (#217) * Add option to disable unsatcore generalization in rel_ind_check * Remove unnecessary assertion -- fix_if_intersects_initial doesn't use solver_ for checking sat * Improve help message * Start frame with property in it, as opposed to keeping property in pre-state of trans (#218) * Improve Refinement in cegar values (#221) * rename files * Revert "rename files" This reverts commit 35107ad. * improve refinement in cegar-values * Fix for constraints after promoting inputvars (#224) * default to true for constraints second arg * Re-populate constraints after promoting input variables * Put everything in the pass * Use updated system * Add a simple test for that issue * Use default inductive_generalization for option 0 in mbic3 (#226) * Add constraints to functional unrolling * Fix off-by-one error in last_model_values * Remove unused symbolic post-image Co-authored-by: Ahmed Irfan <[email protected]> * Pop solver context after cex * Add ic3sa to ic3_variants * Get all possible controlling terms * recursive justify_coi * handle constraints in recursive justify_coi * Fixes in IC3SA (#238) Message: This PR adds a fallback procedure for functional refinement. There's an issue where functional refinement can result in a value due to simplification in the smt-solver. In that case, it will fall back to a simpler refinement approach. Additionally, there are cases (especially when using actual input variables that cannot have lemmas learned over them) where functional refinement can add the same lemma again due to simplification. Another branch (ic3sa-fixes) is experimenting with using a logging solver to avoid that. It also makes sure to learn the lemma which is important for making progress. To do this it uses a relation view of the main transition system. It also splits the constraints into the conjunctive partition for a better unsat core. This PR also fixes an assertion failure that would show up occasionally (more often with mathsat) where the predecessor was over-generalized. There were several iterations to fix this including a recursive justify coi implementation (I think the important part is traversing as a tree instead of a DAG because location of the node matters), and various other attempts. In the end, the only thing that worked was adding all variables appearing in constraints (and in the state update of variables from next constraints). These fixes may be overly conservative, but at least they work and can be improved upon in a separate PR. There is good evidence that this assertion failure no longer occurs (several runs with different random seeds don't turn it up). Unfortunately this is highly non-deterministic so I can't be fully sure. There are still some expected errors when using mathsat as the underlying solver. There appears to be a rewriting bug so that when we create an equality that should be guaranteed to be true in the model (because they had the same value) it ends up being a different term (e.g. rewritten to one that evaluates to false). This bug was already reported and there's not much to do now. However, this seems okay because boolector is better for this algorithm anyway. Commits: * deduplicate labels * comment * Fix in test * Add a new test * Add a fallback refinement procedure * Straightforward substitution * Use relational system in IC3SA for learning path constraints * Minor * Learn path axiom * Value substitution with one input unrolled (state var replaced) * Have two refinement options * Add ic3sa to ic3_variants * Get all possible controlling terms * recursive justify_coi * add constraints * Get a reference * Add learned lemma to trans_label_ * Justify coi for all constraints * Justify next constraint and add a comment * Return new terms when updating abstraction and only add symbols from new terms * Just include all variables from constraints * Fix state update lookup * Minor cleanup * Some clean up * Clarification * Remove empty check of input variable sort * Pass equivalence classes by reference to get updated * Address Ahmed's comment * Add predecessor_generalization_and_fix * Mark IC3SA and IC3IA as having an approximate predecessor generalization * fix * Fix * Guard with extra condition * Update engines/ic3base.cpp Co-authored-by: Ahmed Irfan <[email protected]> * Revert "Update engines/ic3base.cpp" This reverts commit a6f84fc. Co-authored-by: Ahmed Irfan <[email protected]>
makaimann
added a commit
that referenced
this pull request
Jan 30, 2021
* Add SubTermCollector and basic test for it * Temporarily pull a branch of smt-switch * Pull newer smt-switch * Stub out IC3SA implementation * Add refine method -- abstraction not needed, only in form of clauses * Stub out more methods for ic3sa * set up initial abstraction * First pass get_equivalence_classes_from_model implementation * First pass on get_model_ic3formula for IC3SA * First pass on IC3SA::check_ts * First pass on ic3formula_check_valid in IC3SA * remove TODO * Add test for untiming with FunctionalUnroller * Mark FunctionalUnroller::at_time as override * Don't include ITEs in subterm walker by default * Create method is_predicate * Keep track of predicates in subterm walker * Include predicates in ic3formula model for ic3sa * Stub out intersects_bad in IC3SA * First pass at projection in IC3SA * Add a minor comment * Update IC3SA constructor * Remove old NYI exception * Add some todos * First pass on generalize_predecessor for IC3SA * Add a TODO -- not done with generalize_predecessor * Add helper method for removing ITEs under a given model * Recover CEX trace in IC3SA::refine * Fix copy-paste mistake * WIP on refinement in IC3SA * Take and return vectors in remove_ites_under_model * Partial fix for symbolic_post_image * More WIP on refinement * Finish get_model_ic3formula implementation in ic3sa * Add ic3sa engine option * Minor * minor fix * Add debug printing method * Fix in SubTermCollector * Add a todo * Add include_symbols option to is_predicate * Remove some engines from all_engines for now * Fix: don't want both polarities of a literal in get_predicates * Allow literals and predicates in ic3sa ic3formulas * Add option to show invariant * Don't pass verbosity through to COI in ic3sa * Add another simple sample problem * Allow bvnot for eq_lit * Get rid of is_eq_lit * Fix initial substitute method * Minor fix in construct_partition * Add some todos * WIP on refinement * More work on refinement * More WIP on refine * simplify cex trace traversal * Clear proof goals in refinement * Add size method to ProofGoalQueue * Use local logger in fcoi * Logger message for generalize_predecessor * WIP for removing fresh symbolic constants from axiom in refine * Add only curr terms to abstraction * Add method for promoting an input variable to be a state variable * Fix in promote_inputvar * Promote input variables to state variables * Use fresh unrolling from i-1 * Working for two basic examples * Some cleanup * Handle length-one CEX * Add axiom to trans_label_ assumptions * Use one method for adding to term abstraction * Don't combine terms because btor might simplify * Improvements to term analysis for boolector * Hack fix for ic3formula_check_valid with boolector * Fix in check_valid * Add new sample problem * Update debug printing methods * IC3SA fixes: keep track of representatives and intersects_bad generalization might fail * Fix for cube creation * Minor * Fix for is_predicate * Fix in collect subterms * Minor * Add basic test for IC3SA * Minor fix in subterm collector * Updates to IC3SA for prover interface updates * Other fixes to bring in line with changes * Fixes for changes to master * minor * De-duplicate using a set * Add assertions construct_partition * Rely on is_lit from smt-switch * Ic3sa justify coi (#195) * WIP * WIP on justify_coi * First pass implementation on get_controlling * Use justify_coi -- currently failing * Some fixes in justify_coi * Fix in predicate projection * Fix in justify_coi -- still failing an assertion * Another fix for justify_coi: always visit Ite condition * Compilation fix: don't rely on template deduction * Include constraints in justify_coi * Add Implies and refactor for controlling args * Remove unused variable * format * Compilation fixes for upstream changes * Guard interpolant based engines * Add sample file * Fix in justify coi -- filter variables after traversing whole formula * Temporarily remove assertion * Don't replace ITEs because we don't want to fix a path * Use promote inputvars for ic3sa * Increase verbosity for printing axiom * Ic3sa functional (#220) * Add a functional unroller * WIP on functional unrolling refinement * Fix in functional unroller * More WIP on functional unrolling refinement in ic3sa * Turn off assume-prop in pre-state by default (#219) * Move prop_in_trans implementation to cpp * Change default to not assume property in pre-state * IC3Base: Add option to disable unsat core generalization (#217) * Add option to disable unsatcore generalization in rel_ind_check * Remove unnecessary assertion -- fix_if_intersects_initial doesn't use solver_ for checking sat * Improve help message * Start frame with property in it, as opposed to keeping property in pre-state of trans (#218) * Improve Refinement in cegar values (#221) * rename files * Revert "rename files" This reverts commit 35107ad. * improve refinement in cegar-values * Fix for constraints after promoting inputvars (#224) * default to true for constraints second arg * Re-populate constraints after promoting input variables * Put everything in the pass * Use updated system * Add a simple test for that issue * Use default inductive_generalization for option 0 in mbic3 (#226) * Add constraints to functional unrolling * Fix off-by-one error in last_model_values * Remove unused symbolic post-image Co-authored-by: Ahmed Irfan <[email protected]> * Pop solver context after cex * Add ic3sa to ic3_variants * Get all possible controlling terms * recursive justify_coi * handle constraints in recursive justify_coi * Fixes in IC3SA (#238) Message: This PR adds a fallback procedure for functional refinement. There's an issue where functional refinement can result in a value due to simplification in the smt-solver. In that case, it will fall back to a simpler refinement approach. Additionally, there are cases (especially when using actual input variables that cannot have lemmas learned over them) where functional refinement can add the same lemma again due to simplification. Another branch (ic3sa-fixes) is experimenting with using a logging solver to avoid that. It also makes sure to learn the lemma which is important for making progress. To do this it uses a relation view of the main transition system. It also splits the constraints into the conjunctive partition for a better unsat core. This PR also fixes an assertion failure that would show up occasionally (more often with mathsat) where the predecessor was over-generalized. There were several iterations to fix this including a recursive justify coi implementation (I think the important part is traversing as a tree instead of a DAG because location of the node matters), and various other attempts. In the end, the only thing that worked was adding all variables appearing in constraints (and in the state update of variables from next constraints). These fixes may be overly conservative, but at least they work and can be improved upon in a separate PR. There is good evidence that this assertion failure no longer occurs (several runs with different random seeds don't turn it up). Unfortunately this is highly non-deterministic so I can't be fully sure. There are still some expected errors when using mathsat as the underlying solver. There appears to be a rewriting bug so that when we create an equality that should be guaranteed to be true in the model (because they had the same value) it ends up being a different term (e.g. rewritten to one that evaluates to false). This bug was already reported and there's not much to do now. However, this seems okay because boolector is better for this algorithm anyway. Commits: * deduplicate labels * comment * Fix in test * Add a new test * Add a fallback refinement procedure * Straightforward substitution * Use relational system in IC3SA for learning path constraints * Minor * Learn path axiom * Value substitution with one input unrolled (state var replaced) * Have two refinement options * Add ic3sa to ic3_variants * Get all possible controlling terms * recursive justify_coi * add constraints * Get a reference * Add learned lemma to trans_label_ * Justify coi for all constraints * Justify next constraint and add a comment * Return new terms when updating abstraction and only add symbols from new terms * Just include all variables from constraints * Fix state update lookup * Minor cleanup * Some clean up * Try starting with only leaves in abstraction * Try getting a single controlling term after all constraints fix * Add option for ic3sa interpolation -- doesn't do anything yet * Add interpolator support * Get predicates and leaves for starting abstraction * WIP on supporting uf abstraction for IC3SA * Fix refinement for IC3SA * Add a logging solver option * Add option for initial term abstraction -- currently unused * Initial term abstraction is configurable * Revert "Try getting a single controlling term after all constraints fix" This reverts commit 6588de6. * Clarification * Remove empty check of input variable sort * Pass equivalence classes by reference to get updated * Address Ahmed's comment * Revert "Revert "Try getting a single controlling term after all constraints fix"" This reverts commit b23d087. * Minor * Add option to disable functional refinement attempt * Justify the constraints but don't add all the variables up front because of the approx_pregen_ fix * Set base-context-1 for btor logging solver Co-authored-by: Ahmed Irfan <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR fixes a soundness bug that can show up when using option
--promote-inputvars. This is because after promoting input variables to state variables with no next state update (e.g. implicit inputs), we should re-evaluate all the constraints. A constraint that was previously only added over current because it had inputs in it, should now be added over next as well. It was correct before the pass, because input variables are only relevant for a transition, but once they're promoted that's no longer true.Since it is so unsafe to promote input variables directly, this PR removes that functionality of a
TransitionSystem. Instead there is now a pass that (safely) rebuilds the transition system without input variables.Note: This is of course a recurring issue, see #73. I think there could be a better solution long term. Basically, we should pick a representation and stick with it. It is a bit tough because there are some algorithms that do better with all state variables, and others that make more sense to have "true" input variables. In principle, I like both for different reasons. The implicit inputs are the simplest and this is typically the formalism in papers. On the other hand, it's not very intuitive since inputs should not be part of the state representation, and I think it's nice to show syntactically that they're only important for transitions.
Regardless, for now, I think this is a reasonable fix. We can return to this when we have more time.