| .. |
|
arith_axioms.cpp
|
overhaul of proof format for new solver
|
2022-08-28 17:44:33 -07:00 |
|
arith_diagnostics.cpp
|
Add RUP checking mode to proof checker.
|
2022-08-30 09:45:19 -07:00 |
|
arith_internalize.cpp
|
working on reconciling perf for arithmetic solvers
|
2022-07-11 07:38:51 -07:00 |
|
arith_proof_checker.h
|
indentation
|
2022-09-04 16:23:11 -07:00 |
|
arith_solver.cpp
|
add a queue head to delay propagation
|
2022-09-18 17:23:00 -07:00 |
|
arith_solver.h
|
updated header file for arithmetic solver
|
2022-09-18 17:23:00 -07:00 |
|
array_axioms.cpp
|
#6196
|
2022-08-07 10:17:24 +03:00 |
|
array_diagnostics.cpp
|
remove '#include <iostream>' from headers and from unneeded places
|
2022-06-17 14:10:19 +01:00 |
|
array_internalize.cpp
|
drat
|
2022-06-11 09:15:32 -07:00 |
|
array_model.cpp
|
update topological sort to use arrays instead of hash tables, expose Context over Z3Object for programmability
|
2022-06-08 06:28:24 -07:00 |
|
array_solver.cpp
|
add min/max diff in final check
|
2022-05-04 07:39:38 -07:00 |
|
array_solver.h
|
drat
|
2022-06-11 09:15:32 -07:00 |
|
atom2bool_var.cpp
|
improve pre-processing
|
2022-04-15 12:55:26 +02:00 |
|
atom2bool_var.h
|
mbp (#4741)
|
2020-10-21 15:48:40 -07:00 |
|
ba_xor.h
|
arrays (#4684)
|
2020-09-13 19:29:59 -07:00 |
|
bv_ackerman.cpp
|
regression fix to ackerman gc and memory smash, perf fix for handling bv2int axioms, perf fix for filtering ackerman
|
2022-08-26 10:44:33 -07:00 |
|
bv_ackerman.h
|
don't have bv-ackerman influence simplification
|
2022-08-21 15:25:18 -07:00 |
|
bv_delay_internalize.cpp
|
disable bv delay until it is debugged #6324
|
2022-09-07 00:04:57 -07:00 |
|
bv_internalize.cpp
|
indentation
|
2022-09-04 16:23:11 -07:00 |
|
bv_invariant.cpp
|
remove '#include <iostream>' from headers and from unneeded places
|
2022-06-17 14:10:19 +01:00 |
|
bv_solver.cpp
|
log E-matching based quantifier instantiations as hints
|
2022-08-31 18:59:02 -07:00 |
|
bv_solver.h
|
lazy multiplier experiment
|
2022-09-05 03:09:18 -07:00 |
|
CMakeLists.txt
|
overhaul of proof format for new solver
|
2022-08-28 17:44:33 -07:00 |
|
dt_solver.cpp
|
fix #6127 again
|
2022-07-04 12:42:11 -07:00 |
|
dt_solver.h
|
fix #6127 again
|
2022-07-04 12:42:11 -07:00 |
|
euf_ackerman.cpp
|
throttle ackerman on arrays
|
2022-01-01 15:33:33 -08:00 |
|
euf_ackerman.h
|
throttle ackerman on arrays
|
2022-01-01 15:33:33 -08:00 |
|
euf_internalize.cpp
|
fix variable tracking bug in explanations with literals
|
2022-09-01 23:26:38 -07:00 |
|
euf_invariant.cpp
|
#5211
|
2021-04-24 10:28:22 -07:00 |
|
euf_model.cpp
|
na
|
2022-06-08 08:05:19 -07:00 |
|
euf_proof.cpp
|
fix variable tracking bug in explanations with literals
|
2022-09-01 23:26:38 -07:00 |
|
euf_proof_checker.cpp
|
fill in missing pieces of proof hint checker for Farkas and RUP
|
2022-08-31 05:29:15 -07:00 |
|
euf_proof_checker.h
|
fill in missing pieces of proof hint checker for Farkas and RUP
|
2022-08-31 05:29:15 -07:00 |
|
euf_relevancy.cpp
|
setting roots breaks relevancy propagation
|
2022-01-05 21:16:25 -08:00 |
|
euf_relevancy.h
|
more fixes on relevancy
|
2022-01-04 22:02:28 -08:00 |
|
euf_solver.cpp
|
overhaul of proof format for new solver
|
2022-08-28 17:44:33 -07:00 |
|
euf_solver.h
|
build fixes
|
2022-08-28 18:54:36 -07:00 |
|
fpa_solver.cpp
|
use netstandard 2.0 per recommendations
|
2021-12-25 13:44:49 -08:00 |
|
fpa_solver.h
|
#5454
|
2021-08-15 16:48:28 -07:00 |
|
pb_card.cpp
|
streamline pb solver interface and naming after removal of xor
|
2021-02-28 12:32:04 -08:00 |
|
pb_card.h
|
streamline pb solver interface and naming after removal of xor
|
2021-02-28 12:32:04 -08:00 |
|
pb_constraint.cpp
|
streamline pb solver interface and naming after removal of xor
|
2021-02-28 12:32:04 -08:00 |
|
pb_constraint.h
|
Add and fix a few general compiler warnings. (#5628)
|
2021-10-29 15:42:32 +02:00 |
|
pb_internalize.cpp
|
#5753
|
2022-01-15 18:01:31 -08:00 |
|
pb_pb.cpp
|
streamline pb solver interface and naming after removal of xor
|
2021-02-28 12:32:04 -08:00 |
|
pb_pb.h
|
streamline pb solver interface and naming after removal of xor
|
2021-02-28 12:32:04 -08:00 |
|
pb_solver.cpp
|
move drat functionality into euf
|
2022-08-25 19:19:13 -07:00 |
|
pb_solver.h
|
#5753
|
2022-01-15 18:01:31 -08:00 |
|
pb_solver_interface.h
|
Add and fix a few general compiler warnings. (#5628)
|
2021-10-29 15:42:32 +02:00 |
|
q_clause.cpp
|
fixes to sat.euf ematching #5573
|
2021-10-16 15:52:37 -07:00 |
|
q_clause.h
|
#5753
|
2022-01-15 09:35:25 -08:00 |
|
q_ematch.cpp
|
log E-matching based quantifier instantiations as hints
|
2022-08-31 18:59:02 -07:00 |
|
q_ematch.h
|
#5778
|
2022-04-25 11:22:00 +01:00 |
|
q_eval.cpp
|
fix unsoundness in quantifier propagation #6116 and add initial lemma logging
|
2022-08-23 19:10:01 -07:00 |
|
q_eval.h
|
#5753
|
2022-01-15 09:35:25 -08:00 |
|
q_mam.cpp
|
#6116
|
2022-08-07 10:25:04 +03:00 |
|
q_mam.h
|
Use = default for virtual constructors.
|
2022-08-05 18:11:46 +03:00 |
|
q_mbi.cpp
|
rename statistics to something more meaningful: instantiations from MBQI are tagged with mbi
|
2022-09-18 17:23:00 -07:00 |
|
q_mbi.h
|
track instantiations from MBQI in proof logging for new solver
|
2022-09-01 08:51:53 -07:00 |
|
q_model_fixer.cpp
|
Remove empty leaf destructors. (#6211)
|
2022-07-30 10:07:03 +01:00 |
|
q_model_fixer.h
|
Use = default for virtual constructors.
|
2022-08-05 18:11:46 +03:00 |
|
q_queue.cpp
|
enable propagation
|
2022-01-08 19:00:56 -08:00 |
|
q_queue.h
|
redo bindings/fingerprints
|
2021-10-05 10:15:56 -07:00 |
|
q_solver.cpp
|
track instantiations from MBQI in proof logging for new solver
|
2022-09-01 08:51:53 -07:00 |
|
q_solver.h
|
track instantiations from MBQI in proof logging for new solver
|
2022-09-01 08:51:53 -07:00 |
|
recfun_solver.cpp
|
Treat arguments to recursive functions as beta redexes
|
2022-06-14 09:51:06 -07:00 |
|
recfun_solver.h
|
fixing compiler warn (missing override) (#6125)
|
2022-06-30 15:39:28 -07:00 |
|
sat_internalizer.h
|
Use = default for virtual constructors.
|
2022-08-05 18:11:46 +03:00 |
|
sat_smt.h
|
CNF conversion refactoring (#5547)
|
2021-09-20 08:53:10 -07:00 |
|
sat_th.cpp
|
overhaul of proof format for new solver
|
2022-08-28 17:44:33 -07:00 |
|
sat_th.h
|
overhaul of proof format for new solver
|
2022-08-28 17:44:33 -07:00 |
|
user_solver.cpp
|
fix typo
|
2022-07-25 03:44:12 +02:00 |
|
user_solver.h
|
force-push on new_eq, new_diseq in user propagator, other fixes to Python bindings for user propagator
|
2022-07-25 03:42:29 +02:00 |
|
xor_solver.cpp
|
add initial skeleton for xor-solver
|
2022-08-12 11:54:10 -04:00 |
|
xor_solver.d
|
remove xor solver, tune dt_solver for enumeration case
|
2021-02-27 17:17:39 -08:00 |
|
xor_solver.h
|
add initial skeleton for xor-solver
|
2022-08-12 11:54:10 -04:00 |
