Activity
Merge branch 'master' into rewriting-and-inductive-reasoning
Merge branch 'master' into rewriting-and-inductive-reasoning
fixed generalizing and instantiating substitutions for unbound variables
fixed generalizing and instantiating substitutions for unbound variables
escape some things in identifiers, CVC doesn't like them
escape some things in identifiers, CVC doesn't like them
Force push
subtle unsoundness fix related to failure to distinguish between top …
subtle unsoundness fix related to failure to distinguish between top …
Add missing template declarations
Add missing template declarations
ALASCA FM and superposition
ALASCA FM and superposition
fix numerals for cvc5, UWA for binary resolution
fix numerals for cvc5, UWA for binary resolution
get linear terms working
get linear terms working
clear up theory special-cases a bit, factoring and equality resolution
clear up theory special-cases a bit, factoring and equality resolution
clear up theory special-cases a bit, factoring and equality resolution
clear up theory special-cases a bit, factoring and equality resolution
Force push
clear up theory special-cases a bit, factoring and equality resolution
clear up theory special-cases a bit, factoring and equality resolution
strengthened alasca demodulations
strengthened alasca demodulations
strengthened alasca ordering
strengthened alasca ordering
'polyfill' some theory functions
'polyfill' some theory functions
Force push
'polyfill' some theory functions
'polyfill' some theory functions
Make KBO::State static local object
Make KBO::State static local object