| .. |
|
polysat
|
signed_constraint ==
|
2024-03-12 16:26:27 +01:00 |
|
arith_axioms.cpp
|
port fixes to intblast
|
2024-03-09 09:43:14 -08:00 |
|
arith_diagnostics.cpp
|
Api (#7097)
|
2024-01-24 16:05:18 -08:00 |
|
arith_internalize.cpp
|
Api (#7097)
|
2024-01-24 16:05:18 -08:00 |
|
arith_sls.cpp
|
Api (#7097)
|
2024-01-24 16:05:18 -08:00 |
|
arith_sls.h
|
Api (#7097)
|
2024-01-24 16:05:18 -08:00 |
|
arith_solver.cpp
|
Api (#7097)
|
2024-01-24 16:05:18 -08:00 |
|
arith_solver.h
|
Api (#7097)
|
2024-01-24 16:05:18 -08:00 |
|
arith_theory_checker.h
|
update format and checker for implied-eq
|
2023-07-27 13:21:45 -07:00 |
|
arith_value.cpp
|
Add intblast solver
|
2023-12-15 13:50:38 -08:00 |
|
arith_value.h
|
Add intblast solver
|
2023-12-15 13:50:38 -08:00 |
|
array_axioms.cpp
|
install importlib-resources for ubuntu doc
|
2023-12-04 10:33:29 -08:00 |
|
array_diagnostics.cpp
|
|
|
|
array_internalize.cpp
|
remove unused experimental feature - diff
|
2022-10-24 16:13:24 -07:00 |
|
array_model.cpp
|
|
|
|
array_solver.cpp
|
remove unused experimental feature - diff
|
2022-10-24 16:13:24 -07:00 |
|
array_solver.h
|
port Jakob's update to union_find from polysat branch
|
2023-12-18 09:25:24 -08:00 |
|
atom2bool_var.cpp
|
|
|
|
atom2bool_var.h
|
|
|
|
ba_xor.h
|
|
|
|
bv_ackerman.cpp
|
|
|
|
bv_ackerman.h
|
|
|
|
bv_delay_internalize.cpp
|
|
|
|
bv_internalize.cpp
|
port Jakob's update to bv_internalize
|
2023-12-18 09:31:59 -08:00 |
|
bv_invariant.cpp
|
|
|
|
bv_solver.cpp
|
rename antecedent utilities for clarity
|
2023-07-22 11:30:34 -07:00 |
|
bv_solver.h
|
port Jakob's update to union_find from polysat branch
|
2023-12-18 09:25:24 -08:00 |
|
bv_theory_checker.cpp
|
remove once pragma from cpp file
|
2022-10-18 14:57:49 -07:00 |
|
bv_theory_checker.h
|
wip - add bit-vector validator plugins and logging
|
2022-10-18 14:50:21 -07:00 |
|
CMakeLists.txt
|
separate egraph functionality
|
2023-12-22 15:57:28 -08:00 |
|
distinct_theory_checker.h
|
wip - features and bug-fixes to proof logging
|
2022-10-18 07:54:49 -07:00 |
|
dt_solver.cpp
|
fix typos
|
2023-12-18 09:33:40 -08:00 |
|
dt_solver.h
|
fix typos
|
2023-12-18 09:33:40 -08:00 |
|
euf_ackerman.cpp
|
#6364 - remove option of redundant clauses from internalization
|
2022-10-24 00:38:31 -07:00 |
|
euf_ackerman.h
|
|
|
|
euf_internalize.cpp
|
Add intblast solver
|
2023-12-15 13:50:38 -08:00 |
|
euf_invariant.cpp
|
|
|
|
euf_local_search.cpp
|
deal with compiler warnings (unused variables etc)
|
2023-02-18 17:53:37 -08:00 |
|
euf_model.cpp
|
remove windowsArm64 from nightly
|
2023-12-17 10:04:49 -08:00 |
|
euf_proof.cpp
|
fix axiomatization for sdiv
|
2024-01-13 13:10:00 -08:00 |
|
euf_proof_checker.cpp
|
add proof checker plugin
|
2023-12-31 05:30:21 -08:00 |
|
euf_proof_checker.h
|
fix #6637
|
2023-03-22 08:49:33 +01:00 |
|
euf_relevancy.cpp
|
|
|
|
euf_relevancy.h
|
|
|
|
euf_solver.cpp
|
Merge remote-tracking branch 'origin/master' into poly
|
2024-02-26 11:46:22 +01:00 |
|
euf_solver.h
|
Add intblast solver
|
2023-12-15 13:50:38 -08:00 |
|
fpa_solver.cpp
|
#6364 - remove option of redundant clauses from internalization
|
2022-10-24 00:38:31 -07:00 |
|
fpa_solver.h
|
#6364 - remove option of redundant clauses from internalization
|
2022-10-24 00:38:31 -07:00 |
|
intblast_solver.cpp
|
write validation in bv format too
|
2024-03-12 16:18:39 +01:00 |
|
intblast_solver.h
|
pass along lemma name
|
2024-02-26 10:51:01 +01:00 |
|
pb_card.cpp
|
fix #6813 - proofs terms are fragile with respect to simplificiation of not(not(e)). It would be better if proof terms didn't have to track this level of detail, but the legacy proof format assumes strictly checkable proofs. A patch is to fixup terms within the mk_transitivity constructor
|
2023-07-15 17:03:04 -07:00 |
|
pb_card.h
|
Use noexcept more. (#7058)
|
2023-12-16 12:14:53 +00:00 |
|
pb_constraint.cpp
|
|
|
|
pb_constraint.h
|
Use noexcept more. (#7058)
|
2023-12-16 12:14:53 +00:00 |
|
pb_internalize.cpp
|
#6523
|
2023-08-01 08:41:26 -07:00 |
|
pb_pb.cpp
|
#6423
|
2022-10-26 12:06:11 -07:00 |
|
pb_pb.h
|
Use noexcept more. (#7058)
|
2023-12-16 12:14:53 +00:00 |
|
pb_solver.cpp
|
fix #6692
|
2023-04-17 09:11:16 -07:00 |
|
pb_solver.h
|
pass sign into literal definition for pbge
|
2023-01-04 16:55:44 -08:00 |
|
pb_solver_interface.h
|
|
|
|
polysat_egraph.cpp
|
move side effect out of print statement
|
2024-03-11 04:08:07 -07:00 |
|
polysat_internalize.cpp
|
fix extract axiom
|
2024-03-12 13:47:23 +01:00 |
|
polysat_model.cpp
|
pass along lemma name
|
2024-02-26 10:51:01 +01:00 |
|
polysat_solver.cpp
|
pass along lemma name
|
2024-02-26 10:51:01 +01:00 |
|
polysat_solver.h
|
pass along lemma name
|
2024-02-26 10:51:01 +01:00 |
|
polysat_theory_checker.h
|
add proof checker plugin
|
2023-12-31 05:30:21 -08:00 |
|
q_clause.cpp
|
|
|
|
q_clause.h
|
log also quantifier generation (besides binding)
|
2022-10-20 17:49:15 -07:00 |
|
q_ematch.cpp
|
track quantifier instantiation method in proof hint #7080
|
2024-01-20 17:44:07 -08:00 |
|
q_ematch.h
|
track quantifier instantiation method in proof hint #7080
|
2024-01-20 17:44:07 -08:00 |
|
q_eval.cpp
|
address compiler warnings, and user question #6544
|
2023-01-19 19:02:43 -08:00 |
|
q_eval.h
|
|
|
|
q_mam.cpp
|
address compiler warnings, and user question #6544
|
2023-01-19 19:02:43 -08:00 |
|
q_mam.h
|
|
|
|
q_mbi.cpp
|
track quantifier instantiation method in proof hint #7080
|
2024-01-20 17:44:07 -08:00 |
|
q_mbi.h
|
track quantifier instantiation method in proof hint #7080
|
2024-01-20 17:44:07 -08:00 |
|
q_model_fixer.cpp
|
#6364
|
2022-10-20 16:39:43 -07:00 |
|
q_model_fixer.h
|
|
|
|
q_queue.cpp
|
|
|
|
q_queue.h
|
|
|
|
q_solver.cpp
|
fix build warnings
|
2024-02-01 09:36:52 -08:00 |
|
q_solver.h
|
track quantifier instantiation method in proof hint #7080
|
2024-01-20 17:44:07 -08:00 |
|
q_theory_checker.cpp
|
#6364
|
2022-10-20 16:39:43 -07:00 |
|
q_theory_checker.h
|
|
|
|
recfun_solver.cpp
|
#6364 - remove option of redundant clauses from internalization
|
2022-10-24 00:38:31 -07:00 |
|
recfun_solver.h
|
#6364 - remove option of redundant clauses from internalization
|
2022-10-24 00:38:31 -07:00 |
|
sat_internalizer.h
|
fix #6623
|
2023-04-09 21:10:24 -07:00 |
|
sat_smt.h
|
|
|
|
sat_th.cpp
|
update format and checker for implied-eq
|
2023-07-27 13:23:17 -07:00 |
|
sat_th.h
|
minor changes
|
2024-02-08 15:25:00 +01:00 |
|
specrel_solver.cpp
|
add EUF plugin framework.
|
2023-11-30 13:58:30 -08:00 |
|
specrel_solver.h
|
add EUF plugin framework.
|
2023-11-30 13:58:30 -08:00 |
|
tseitin_theory_checker.cpp
|
strengthen Tseitin checker to take true/false constants into account
|
2023-07-28 16:54:33 -07:00 |
|
tseitin_theory_checker.h
|
wip - proof checking, add support for distinct, other fixes
|
2022-10-17 17:51:10 -07:00 |
|
user_solver.cpp
|
add clause persistence to sat/smt solver
|
2024-02-04 16:42:10 -08:00 |
|
user_solver.h
|
add clause persistence to sat/smt solver
|
2024-02-04 16:42:10 -08:00 |
|
xor_solver.cpp
|
wip - remove stale skaffolding for retrieving sub-hints.
|
2022-10-16 17:18:08 -07:00 |
|
xor_solver.d
|
|
|
|
xor_solver.h
|
fix build
|
2022-10-24 10:23:50 +01:00 |
