projects
/
cvc5.git
/ tree
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
| tree
history
|
HEAD
Use inference manager for nl_solver (#5125)
[cvc5.git]
/
src
/
theory
/
drwxr-xr-x
..
-rw-r--r--
1589
CMakeLists.txt
blob
|
history
|
raw
drwxr-xr-x
-
arith
tree
|
history
drwxr-xr-x
-
arrays
tree
|
history
-rw-r--r--
794
assertion.cpp
blob
|
history
|
raw
-rw-r--r--
1550
assertion.h
blob
|
history
|
raw
-rw-r--r--
2597
atom_requests.cpp
blob
|
history
|
raw
-rw-r--r--
3127
atom_requests.h
blob
|
history
|
raw
drwxr-xr-x
-
bags
tree
|
history
drwxr-xr-x
-
booleans
tree
|
history
drwxr-xr-x
-
builtin
tree
|
history
drwxr-xr-x
-
bv
tree
|
history
-rw-r--r--
1664
care_graph.h
blob
|
history
|
raw
-rw-r--r--
3153
combination_care_graph.cpp
blob
|
history
|
raw
-rw-r--r--
1446
combination_care_graph.h
blob
|
history
|
raw
-rw-r--r--
3800
combination_engine.cpp
blob
|
history
|
raw
-rw-r--r--
4723
combination_engine.h
blob
|
history
|
raw
drwxr-xr-x
-
datatypes
tree
|
history
-rw-r--r--
3406
decision_manager.cpp
blob
|
history
|
raw
-rw-r--r--
5740
decision_manager.h
blob
|
history
|
raw
-rw-r--r--
3989
decision_strategy.cpp
blob
|
history
|
raw
-rw-r--r--
4921
decision_strategy.h
blob
|
history
|
raw
-rw-r--r--
4285
eager_proof_generator.cpp
blob
|
history
|
raw
-rw-r--r--
7045
eager_proof_generator.h
blob
|
history
|
raw
-rw-r--r--
1492
ee_manager.cpp
blob
|
history
|
raw
-rw-r--r--
3197
ee_manager.h
blob
|
history
|
raw
-rw-r--r--
3460
ee_manager_distributed.cpp
blob
|
history
|
raw
-rw-r--r--
3447
ee_manager_distributed.h
blob
|
history
|
raw
-rw-r--r--
1590
ee_setup_info.h
blob
|
history
|
raw
-rw-r--r--
6642
engine_output_channel.cpp
blob
|
history
|
raw
-rw-r--r--
3684
engine_output_channel.h
blob
|
history
|
raw
-rw-r--r--
29374
evaluator.cpp
blob
|
history
|
raw
-rw-r--r--
5574
evaluator.h
blob
|
history
|
raw
-rw-r--r--
16021
ext_theory.cpp
blob
|
history
|
raw
-rw-r--r--
11892
ext_theory.h
blob
|
history
|
raw
drwxr-xr-x
-
fp
tree
|
history
-rw-r--r--
3882
inference_manager_buffered.cpp
blob
|
history
|
raw
-rw-r--r--
5324
inference_manager_buffered.h
blob
|
history
|
raw
-rw-r--r--
1612
interrupted.h
blob
|
history
|
raw
-rw-r--r--
21130
logic_info.cpp
blob
|
history
|
raw
-rw-r--r--
9242
logic_info.h
blob
|
history
|
raw
-rwxr-xr-x
6208
mkrewriter
blob
|
history
|
raw
-rwxr-xr-x
10102
mktheorytraits
blob
|
history
|
raw
-rw-r--r--
6596
model_manager.cpp
blob
|
history
|
raw
-rw-r--r--
5827
model_manager.h
blob
|
history
|
raw
-rw-r--r--
3577
model_manager_distributed.cpp
blob
|
history
|
raw
-rw-r--r--
2138
model_manager_distributed.h
blob
|
history
|
raw
-rw-r--r--
2927
output_channel.cpp
blob
|
history
|
raw
-rw-r--r--
8240
output_channel.h
blob
|
history
|
raw
drwxr-xr-x
-
quantifiers
tree
|
history
-rw-r--r--
41463
quantifiers_engine.cpp
blob
|
history
|
raw
-rw-r--r--
16434
quantifiers_engine.h
blob
|
history
|
raw
-rw-r--r--
8246
relevance_manager.cpp
blob
|
history
|
raw
-rw-r--r--
6249
relevance_manager.h
blob
|
history
|
raw
-rw-r--r--
12465
rep_set.cpp
blob
|
history
|
raw
-rw-r--r--
11655
rep_set.h
blob
|
history
|
raw
-rw-r--r--
15935
rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
7591
rewriter.h
blob
|
history
|
raw
-rw-r--r--
2608
rewriter_attributes.h
blob
|
history
|
raw
-rw-r--r--
2457
rewriter_tables_template.h
blob
|
history
|
raw
drwxr-xr-x
-
sep
tree
|
history
drwxr-xr-x
-
sets
tree
|
history
-rw-r--r--
3560
shared_solver.cpp
blob
|
history
|
raw
-rw-r--r--
4740
shared_solver.h
blob
|
history
|
raw
-rw-r--r--
2859
shared_solver_distributed.cpp
blob
|
history
|
raw
-rw-r--r--
2271
shared_solver_distributed.h
blob
|
history
|
raw
-rw-r--r--
9722
shared_terms_database.cpp
blob
|
history
|
raw
-rw-r--r--
8168
shared_terms_database.h
blob
|
history
|
raw
-rw-r--r--
3405
smt_engine_subsolver.cpp
blob
|
history
|
raw
-rw-r--r--
3109
smt_engine_subsolver.h
blob
|
history
|
raw
-rw-r--r--
31128
sort_inference.cpp
blob
|
history
|
raw
-rw-r--r--
6023
sort_inference.h
blob
|
history
|
raw
drwxr-xr-x
-
strings
tree
|
history
-rw-r--r--
13289
subs_minimize.cpp
blob
|
history
|
raw
-rw-r--r--
3464
subs_minimize.h
blob
|
history
|
raw
-rw-r--r--
8860
substitutions.cpp
blob
|
history
|
raw
-rw-r--r--
5552
substitutions.h
blob
|
history
|
raw
-rw-r--r--
12463
term_registration_visitor.cpp
blob
|
history
|
raw
-rw-r--r--
4085
term_registration_visitor.h
blob
|
history
|
raw
-rw-r--r--
17280
theory.cpp
blob
|
history
|
raw
-rw-r--r--
33036
theory.h
blob
|
history
|
raw
-rw-r--r--
66163
theory_engine.cpp
blob
|
history
|
raw
-rw-r--r--
23990
theory_engine.h
blob
|
history
|
raw
-rw-r--r--
3692
theory_engine_proof_generator.cpp
blob
|
history
|
raw
-rw-r--r--
2787
theory_engine_proof_generator.h
blob
|
history
|
raw
-rw-r--r--
2244
theory_eq_notify.h
blob
|
history
|
raw
-rw-r--r--
4273
theory_id.cpp
blob
|
history
|
raw
-rw-r--r--
3047
theory_id.h
blob
|
history
|
raw
-rw-r--r--
1933
theory_inference.cpp
blob
|
history
|
raw
-rw-r--r--
4478
theory_inference.h
blob
|
history
|
raw
-rw-r--r--
14386
theory_inference_manager.cpp
blob
|
history
|
raw
-rw-r--r--
18163
theory_inference_manager.h
blob
|
history
|
raw
-rw-r--r--
25547
theory_model.cpp
blob
|
history
|
raw
-rw-r--r--
19197
theory_model.h
blob
|
history
|
raw
-rw-r--r--
47321
theory_model_builder.cpp
blob
|
history
|
raw
-rw-r--r--
13452
theory_model_builder.h
blob
|
history
|
raw
-rw-r--r--
13285
theory_preprocessor.cpp
blob
|
history
|
raw
-rw-r--r--
3940
theory_preprocessor.h
blob
|
history
|
raw
-rw-r--r--
6418
theory_proof_step_buffer.cpp
blob
|
history
|
raw
-rw-r--r--
4163
theory_proof_step_buffer.h
blob
|
history
|
raw
-rw-r--r--
1488
theory_registrar.h
blob
|
history
|
raw
-rw-r--r--
2088
theory_rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
4181
theory_rewriter.h
blob
|
history
|
raw
-rw-r--r--
3065
theory_state.cpp
blob
|
history
|
raw
-rw-r--r--
3426
theory_state.h
blob
|
history
|
raw
-rw-r--r--
3414
theory_test_utils.h
blob
|
history
|
raw
-rw-r--r--
1338
theory_traits_template.h
blob
|
history
|
raw
-rw-r--r--
4060
trust_node.cpp
blob
|
history
|
raw
-rw-r--r--
5965
trust_node.h
blob
|
history
|
raw
-rw-r--r--
5430
type_enumerator.h
blob
|
history
|
raw
-rw-r--r--
1373
type_enumerator_template.cpp
blob
|
history
|
raw
-rw-r--r--
2958
type_set.cpp
blob
|
history
|
raw
-rw-r--r--
2805
type_set.h
blob
|
history
|
raw
drwxr-xr-x
-
uf
tree
|
history
-rw-r--r--
4849
valuation.cpp
blob
|
history
|
raw
-rw-r--r--
5574
valuation.h
blob
|
history
|
raw