ALASCA #649
ALASCA #649
Conversation
and literals incomparable
| if (prb.hasInterpretedOperations() || env.signature->hasTermAlgebras()){ | ||
| // Normalizer is needed, because the TheoryAxioms code assumes Normalized problem | ||
| InterpretedNormalizer().apply(prb); |
There was a problem hiding this comment.
Have you considered whether it's a problem for the non-alasca strategies that we no longer do InterpretedNormalizer here?
I mean, in the light of
"// Normalizer is needed, because the TheoryAxioms code assumes Normalized problem"
There was a problem hiding this comment.
Hmmm good question. I can't quite remember when/why i removed this.
I did loads of randomized testing, so I think potential issues should have showed up. Maybe we should also do a regression test checking whether the performance of the old portfolios matches the new one just to be sure i didn't end up skipping adding some theory axioms that were necessary by changing that.
In order to be safe we could also do a guarded normalization with if(!env.options->alasca())... But I think it's probably not necessary. What do you think?
There was a problem hiding this comment.
Yes, that's the line of thinking I was hinting at!
We had several issues in the past with the arithmetic code not doing what it should (performance-wise), because our pipeline was silently broken is such subtle ways like missing normalization steps at strange places during preprocessing. It's a good idea to do a performance regression. (And we should probably go through the pain of trying out both the old approach and alasca, to have them compared during spidering, before saying good buy to the old one completely.)
| @@ -437,16 +428,16 @@ class DHMap | |||
| * If there is a value stored under the @b key, remove | |||
| * it and return true. Otherwise, return false. | |||
| */ | |||
There was a problem hiding this comment.
Could you please also update the comment?
| @@ -398,7 +398,7 @@ Inference::Inference(const FormulaTransformation& ft) { | |||
| init1(ft.rule,ft.premise); | |||
|
|
|||
| ASS_REP(isFormulaTransformation(ft.rule),ruleName(ft.rule)); | |||
| ASS(!ft.premise->isClause()); | |||
| // ASS(!ft.premise->isClause()); // TODO: should this assertion be here? it would keeps us from preprocessing clauses in InterpretedNormalizer | |||
There was a problem hiding this comment.
The idea was: if you apply this to clauses, don't call it a FormulaTransformation.
Do you have a use case for calling FormulaTransformation on clauses? (I mean, it sounds sensible, but if that's the case, let's maybe think if we can single it out and assign it a different inference rule as well!)
This PR contains ALASCA (Abstracting Linear Arithmetic Superposition CAlculus TACAS 2023).
It contains a full-fetched calculus: a couple of inference rules (
Inferences/ALASCA/*), some new term orderings, a new preprocessor, and a couple of files with code shared among inferences ,orderings, and preprocessing.Further it adds a git submodule for VIRAS (LPAR 2024) which is included as an inference rule inside of ALASCA.
In this PR we merge the finished real-arithmetic ALASCA, as well as unfinished (but sound & well-tested) extensions to mixed integer-real arithmetic. These extensions are not yet stable, but will be finished and stabilized very soon.
The options added in this PR:
-uwaalasca_one_interp,alasca_can_abstract,alasca_main: strategies used for the real-arithmetic version of alasca (LPAR2023 paper "Refining Unification with Abstraction")alasca_main_floor: extension ofalasca_mainto mixed arithmetic. unstableofffor-ev: evaluation can now be turned off.-toqkboordering asd described in the ALASCA paperlakbonew ordering that works for mixed arithmetic unstableincompmakes any two terms incomparable. useful for debugging (e.g. checking if the ordering you are developing is incomplete)-viras [ on | off ]Turns on/off the VIRAS inference rule. this option is for mixed arithmetic and unstable-alasca_demodulation [ on | off ]specialized demodulation rule for alsca. this option is not yet well-tested and unstable[ --alasca_strong_normalziation | -alasca_sn ] [ on | off ]enables rewritess >= t ==> s > t | s == tands != t ==> s > t | t > s[ --alasca_integer_conversion | -alascai ] [ on | off ]enables mixed integer-real reasoning in alasca. this option is unstable[ --alasca_abstraction | -alascaa ] [ on | off ]enables abstraction rules needed in corner cases when reasoning about mixed integer-real arithmetic. this option is unstable-p smt2_proofcheck, outputs the proof in a format where every function applicaiton is translated to an smt call. this is not very clean and stable but practically it helps a lot for proof-checking ALASCA proofs using other smt solvers like cvc5.Further changes to the codebase are the following:
DBG_INDENTmacro. This macro can be in any block{ DBG_INDENT; /* ... */ }and all nestedDBGoutputs will be indented by 1 (+ 1 for every envlosing block with DBG_INDENT). this can be helpful for nice debug output in recursive-ish functions.-p smt2_proofcheck, outputs the proof in a format where every function applicaiton is translated to an smt call. this is not very clean and stable but practically it helps a lot for proof-checking ALASCA proofs using other smt solvers like cvc5.qkbowas added to a couple of functions inKernel/KBO*andKernel/Ordering*. This parameter is needed to adjust the precedence relation and the weight function ofKBOand the underlying classes to work as expected byQKbo. The parameter should just be forwarded down to the places where it's needed (constructor of PresedenceOrdering and querying function weights in kbo)--show_theory_axioms on.The code of this PR has been extensively tested with random option combination runs over all of TPTP and SMTLIB.