BSD 3-Clause License -------------------- ethos-ethos-0.1.0/COPYING Unknown or generated -------------------- ethos-ethos-0.1.0/.clang-format ethos-ethos-0.1.0/.github/workflows/main.yml ethos-ethos-0.1.0/AUTHORS ethos-ethos-0.1.0/CMakeLists.txt ethos-ethos-0.1.0/NEWS.md ethos-ethos-0.1.0/README.md ethos-ethos-0.1.0/TODO.txt ethos-ethos-0.1.0/cmake/FindGMP.cmake ethos-ethos-0.1.0/contrib/alfc_compile ethos-ethos-0.1.0/contrib/alfc_gen_and_check.sh ethos-ethos-0.1.0/contrib/alfc_test_compile ethos-ethos-0.1.0/plugins/cpp_compiler/README.md ethos-ethos-0.1.0/plugins/cpp_compiler/compiled.cpp ethos-ethos-0.1.0/plugins/cpp_compiler/compiler.cpp ethos-ethos-0.1.0/plugins/cpp_compiler/compiler.h ethos-ethos-0.1.0/plugins/cpp_compiler/executor.cpp ethos-ethos-0.1.0/plugins/cpp_compiler/executor.h ethos-ethos-0.1.0/smtlibTests/cong.smt2 ethos-ethos-0.1.0/smtlibTests/cong_arith.smt2 ethos-ethos-0.1.0/smtlibTests/datatype.smt2 ethos-ethos-0.1.0/smtlibTests/define-fun.smt2 ethos-ethos-0.1.0/smtlibTests/haniel.smt2 ethos-ethos-0.1.0/smtlibTests/haniel2.smt2 ethos-ethos-0.1.0/smtlibTests/mini-unsat.smt2 ethos-ethos-0.1.0/smtlibTests/perf/SEQ009_size8.smt2 ethos-ethos-0.1.0/smtlibTests/perf/SEQ011_size3.smt2 ethos-ethos-0.1.0/smtlibTests/perf/hole7.cvc.smt2 ethos-ethos-0.1.0/smtlibTests/policy_variable.smt2 ethos-ethos-0.1.0/smtlibTests/quant-sk.smt2 ethos-ethos-0.1.0/smtlibTests/re_unfold_pos.smt2 ethos-ethos-0.1.0/smtlibTests/resolve.smt2 ethos-ethos-0.1.0/smtlibTests/simple-quant.smt2 ethos-ethos-0.1.0/src/CMakeLists.txt ethos-ethos-0.1.0/src/attr.cpp ethos-ethos-0.1.0/src/attr.h ethos-ethos-0.1.0/src/base/check.cpp ethos-ethos-0.1.0/src/base/check.h ethos-ethos-0.1.0/src/base/output.cpp ethos-ethos-0.1.0/src/base/output.h ethos-ethos-0.1.0/src/base/run.cpp ethos-ethos-0.1.0/src/base/run.h ethos-ethos-0.1.0/src/cmd_parser.cpp ethos-ethos-0.1.0/src/cmd_parser.h ethos-ethos-0.1.0/src/expr.cpp ethos-ethos-0.1.0/src/expr.h ethos-ethos-0.1.0/src/expr_info.h ethos-ethos-0.1.0/src/expr_parser.cpp ethos-ethos-0.1.0/src/expr_parser.h ethos-ethos-0.1.0/src/expr_trie.h ethos-ethos-0.1.0/src/input.cpp ethos-ethos-0.1.0/src/input.h ethos-ethos-0.1.0/src/kind.cpp ethos-ethos-0.1.0/src/kind.h ethos-ethos-0.1.0/src/lexer.cpp ethos-ethos-0.1.0/src/lexer.h ethos-ethos-0.1.0/src/literal.cpp ethos-ethos-0.1.0/src/literal.h ethos-ethos-0.1.0/src/main.cpp ethos-ethos-0.1.0/src/parser.cpp ethos-ethos-0.1.0/src/parser.h ethos-ethos-0.1.0/src/plugin.h ethos-ethos-0.1.0/src/state.cpp ethos-ethos-0.1.0/src/state.h ethos-ethos-0.1.0/src/stats.cpp ethos-ethos-0.1.0/src/stats.h ethos-ethos-0.1.0/src/tokens.cpp ethos-ethos-0.1.0/src/tokens.h ethos-ethos-0.1.0/src/type_checker.cpp ethos-ethos-0.1.0/src/type_checker.h ethos-ethos-0.1.0/src/util/bitvector.cpp ethos-ethos-0.1.0/src/util/bitvector.h ethos-ethos-0.1.0/src/util/filesystem.cpp ethos-ethos-0.1.0/src/util/filesystem.h ethos-ethos-0.1.0/src/util/integer.cpp ethos-ethos-0.1.0/src/util/integer.h ethos-ethos-0.1.0/src/util/rational.cpp ethos-ethos-0.1.0/src/util/rational.h ethos-ethos-0.1.0/src/util/string.cpp ethos-ethos-0.1.0/src/util/string.h ethos-ethos-0.1.0/tests/Arith-rules.eo ethos-ethos-0.1.0/tests/Arith-theory.eo ethos-ethos-0.1.0/tests/Booleans-rules.eo ethos-ethos-0.1.0/tests/Bools.eo ethos-ethos-0.1.0/tests/Builtin-rules.eo ethos-ethos-0.1.0/tests/Builtin-theory.eo ethos-ethos-0.1.0/tests/CMakeLists.txt ethos-ethos-0.1.0/tests/Datatypes-theory.eo ethos-ethos-0.1.0/tests/Nary.eo ethos-ethos-0.1.0/tests/Quantifiers-rules.eo ethos-ethos-0.1.0/tests/Quantifiers-theory.eo ethos-ethos-0.1.0/tests/Sets-theory.eo ethos-ethos-0.1.0/tests/Strings-programs.eo ethos-ethos-0.1.0/tests/Strings-theory.eo ethos-ethos-0.1.0/tests/Uf-rules.eo ethos-ethos-0.1.0/tests/Utils.eo ethos-ethos-0.1.0/tests/and-intro-old.eo ethos-ethos-0.1.0/tests/arith-eval.eo ethos-ethos-0.1.0/tests/arith-rules-test.eo ethos-ethos-0.1.0/tests/arity-overload.eo ethos-ethos-0.1.0/tests/axiom-implicit.eo ethos-ethos-0.1.0/tests/beta-reduce-define-fun.eo ethos-ethos-0.1.0/tests/binder-ex.eo ethos-ethos-0.1.0/tests/binder-subterm-share.eo ethos-ethos-0.1.0/tests/bv-concat.eo ethos-ethos-0.1.0/tests/bv-dep-type.eo ethos-ethos-0.1.0/tests/bv-eval.eo ethos-ethos-0.1.0/tests/bv-extract-smt3.eo ethos-ethos-0.1.0/tests/bv-extract.eo ethos-ethos-0.1.0/tests/bv-literals.eo ethos-ethos-0.1.0/tests/bv-type-strict.eo ethos-ethos-0.1.0/tests/chainable.eo ethos-ethos-0.1.0/tests/conclusion-spec.eo ethos-ethos-0.1.0/tests/constant-eval-args.eo ethos-ethos-0.1.0/tests/constant-eval.eo ethos-ethos-0.1.0/tests/datatype-simple.eo ethos-ethos-0.1.0/tests/define-const-simple.eo ethos-ethos-0.1.0/tests/define-fun-dep-type.eo ethos-ethos-0.1.0/tests/define-fun.alfc.eo ethos-ethos-0.1.0/tests/define-sort-iarray.eo ethos-ethos-0.1.0/tests/disamb-arith.eo ethos-ethos-0.1.0/tests/distinct_value_testers.eo ethos-ethos-0.1.0/tests/emptylist.eo ethos-ethos-0.1.0/tests/eval-inc.eo ethos-ethos-0.1.0/tests/evaluate.eo ethos-ethos-0.1.0/tests/evaluation.eo ethos-ethos-0.1.0/tests/examples-booleans.eo ethos-ethos-0.1.0/tests/examples-nary.eo ethos-ethos-0.1.0/tests/ff-nil.eo ethos-ethos-0.1.0/tests/generic-swap.eo ethos-ethos-0.1.0/tests/gt_eval.eo ethos-ethos-0.1.0/tests/ite-compile-test.eo ethos-ethos-0.1.0/tests/let-binder-ex.eo ethos-ethos-0.1.0/tests/literals.eo ethos-ethos-0.1.0/tests/match-simple.eo ethos-ethos-0.1.0/tests/match-variants.eo ethos-ethos-0.1.0/tests/mixed-arith.eo ethos-ethos-0.1.0/tests/mutual-rec.eo ethos-ethos-0.1.0/tests/naive-nary.eo ethos-ethos-0.1.0/tests/nat-type.eo ethos-ethos-0.1.0/tests/nground-nil-v3.eo ethos-ethos-0.1.0/tests/not_and.eo ethos-ethos-0.1.0/tests/opaque-inst.eo ethos-ethos-0.1.0/tests/opaque-inst2.eo ethos-ethos-0.1.0/tests/or-concat-false.eo ethos-ethos-0.1.0/tests/or-list-null-term.eo ethos-ethos-0.1.0/tests/or-list.eo ethos-ethos-0.1.0/tests/or-repl-all-basic.eo ethos-ethos-0.1.0/tests/or-repl-all.eo ethos-ethos-0.1.0/tests/or-variant.eo ethos-ethos-0.1.0/tests/oracle-ex.eo ethos-ethos-0.1.0/tests/oracle-ex2.eo ethos-ethos-0.1.0/tests/oracle_true ethos-ethos-0.1.0/tests/overloading-arith.eo ethos-ethos-0.1.0/tests/overloading-as.eo ethos-ethos-0.1.0/tests/overloading-binder.eo ethos-ethos-0.1.0/tests/overloading.eo ethos-ethos-0.1.0/tests/pairwise.eo ethos-ethos-0.1.0/tests/par-dt.eo ethos-ethos-0.1.0/tests/pf-arith-eval.eo ethos-ethos-0.1.0/tests/pf-haniel.eo ethos-ethos-0.1.0/tests/pf-quant.eo ethos-ethos-0.1.0/tests/pf-sig-replAll.eo ethos-ethos-0.1.0/tests/pf-simple-sig-2.eo ethos-ethos-0.1.0/tests/pf-simple-sig.eo ethos-ethos-0.1.0/tests/pf-substitution-large.eo ethos-ethos-0.1.0/tests/pf-substitution-over-or.eo ethos-ethos-0.1.0/tests/pf-substitution.eo ethos-ethos-0.1.0/tests/premise-list-cong-2.eo ethos-ethos-0.1.0/tests/premise-list-cong.eo ethos-ethos-0.1.0/tests/premise-list-empty.eo ethos-ethos-0.1.0/tests/premise-list-nary-cong-2.eo ethos-ethos-0.1.0/tests/premise-list-nary-cong.eo ethos-ethos-0.1.0/tests/push-pop.eo ethos-ethos-0.1.0/tests/quant-sk-small.alfc.eo ethos-ethos-0.1.0/tests/quant.eo ethos-ethos-0.1.0/tests/quoted.eo ethos-ethos-0.1.0/tests/rare-example.eo ethos-ethos-0.1.0/tests/requires.eo ethos-ethos-0.1.0/tests/right-assoc-variants.eo ethos-ethos-0.1.0/tests/scopes.eo ethos-ethos-0.1.0/tests/self-requires.eo ethos-ethos-0.1.0/tests/sig-replAll.eo ethos-ethos-0.1.0/tests/simple-include.eo ethos-ethos-0.1.0/tests/simple-pf-implicit.eo ethos-ethos-0.1.0/tests/simple-pf.eo ethos-ethos-0.1.0/tests/simple-pf2.eo ethos-ethos-0.1.0/tests/simple-program.eo ethos-ethos-0.1.0/tests/simple-sig-2.eo ethos-ethos-0.1.0/tests/simple-sig.eo ethos-ethos-0.1.0/tests/simple.eo ethos-ethos-0.1.0/tests/simple_uf.eo ethos-ethos-0.1.0/tests/skolemize-v1.eo ethos-ethos-0.1.0/tests/skolemize-v2.eo ethos-ethos-0.1.0/tests/sorry.eo ethos-ethos-0.1.0/tests/str-eval.eo ethos-ethos-0.1.0/tests/strings-rules-test.eo ethos-ethos-0.1.0/tests/substitution-binary-only.eo ethos-ethos-0.1.0/tests/substitution-opaque.eo ethos-ethos-0.1.0/tests/substitution-over-or.eo ethos-ethos-0.1.0/tests/substitution.eo ethos-ethos-0.1.0/tests/theory-rewrite-native.eo ethos-ethos-0.1.0/tests/tiny_oracle.eo ethos-ethos-0.1.0/tests/tiny_oracle.sh ethos-ethos-0.1.0/tests/to_string.eo ethos-ethos-0.1.0/tests/typeof.eo ethos-ethos-0.1.0/tests/use-match.eo ethos-ethos-0.1.0/tests/var-binders-syntax.eo ethos-ethos-0.1.0/type_system_sketch.txt ethos-ethos-0.1.0/user_manual.md