Arie Gurfinkel
05c8067392
Changed pob queue management strategy in spacer_context
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
a696a40a3a
Refactoring
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
ec8f99fee7
Rename expand_node --> expand_pob
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
3f9b5bce99
Remove debug function
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
ac3bbed311
Remove dead code in spacer_manager
...
- removed bg_assertions. Incompatible with mbp in spacer
- removed unique number. Unused
- removed mk_and() and switched to ast_util:mk_and() instead
spacer_manager::mk_and() uses bool_rewriter to simplify the
conjunction
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
33466c75a6
mss loop in prop_solver
...
max sat assignment (mss) to replace core-based maxsmt()
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
d379b14942
Cleanup spacer_iuc_solver
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
fd13eb9e0e
Final cleanup of hypothesis_reducer
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
9d4784baf6
Fix dealloc order in hypotheses_reducer::reset()
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
689414d055
Fix debug printing in iuc_solver
2018-06-14 16:08:48 -07:00
Nikolaj Bjorner
ff0f257102
remove iff
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:48 -07:00
Nikolaj Bjorner
ecf15ab07d
add model_evaluator_util features to model_evalautor
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
8d312f9d1f
Cleanup of hypothesis_reducer
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
2db38fedd6
Cleanup of theory_axiom_reducer proof trasfomation
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
07ad67ebad
Move proof dot printing into iuc_proof
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
45500ff7d3
Cleanup iuc_proof
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
abe67705d3
Cleanup iuc_proof
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
ebf6b18821
maxsat standalone mode
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
49821e7c91
Revised solver_pool
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
c893740e13
Fix compilation
2018-06-14 16:08:48 -07:00
Nikolaj Bjorner
b649cd93cb
change pool solver to enable external control of pool allocation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:48 -07:00
Nikolaj Bjorner
ffdefa4f65
add todo
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
3bc3b00fdd
Post merge compile fixes
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
649bab2f58
Rename itp_solver into iuc_solver
...
IUC stands for Interpolanted UNSAT Core
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
5d3b515a50
Cleanup option names and default values
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
39bdecf9c2
Minor code cleanup
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
83adb6742e
Remove whitespace
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
7c727ee922
Fix compiler warnings
2018-06-14 16:08:48 -07:00
Bernhard Gleiss
4b6921dffb
removed unnecessary assignment
2018-06-14 16:08:48 -07:00
Bernhard Gleiss
295d16bfae
Rewrite hyp-reducer
...
This is a new version that conceptually addresses the bugs in
all previous version. However, it had a hard-to-debug memory
corruption. The bug appeared only in optimized compilation under
Linux with GCC.
This code is suspect and should be reviewed and further tested
2018-06-14 16:08:48 -07:00
Bernhard Gleiss
85c58e344c
Add option to use old_hyp_reducer
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
f0f75d5254
Wire in arith-axiom-reducer
2018-06-14 16:08:48 -07:00
Bernhard Gleiss
0f25e9e831
Moved farkas stats printing to before and after the hyp-reduction
2018-06-14 16:08:48 -07:00
Bernhard Gleiss
de31b07008
arith-theory-axiom reducer to handle arithmetic axioms
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
df2eb771ef
Fix in spacer_itp_solver: use pr.get() instead of get_proof()
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
ab3a6702af
Fix several bugs in hyp_reducer
...
- compute_marks didn't find all units
- call to m.mk_unit_resolution expects that there is at least one unit
- hyp-reduced proof wasn't used
- bug in early termination
- any hypothesis was replaced with the old derivation of the literal
- handle the case of a single literal premise under hypothesis that is
replaced by an empty clause under hypothesis
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
56114a5f6d
Refactor iuc_proof as a separate class
...
This also adds DOT printing support to interpolating proofs
(color for different parts)
iuc_proof is a proof used for IUC computation
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
10106e8e12
Minor fixes to ast_pp_dot
2018-06-14 16:08:48 -07:00
Bernhard Gleiss
247c570e6b
Debug sanity check in spacer_context
...
Triggered by bugs in hypothesis remover
only sanitycheck lemmas in debug-mode
2018-06-14 16:08:48 -07:00
Matteo Marescotti
a4e67b8bb6
Wire JSON printing into Spacer
2018-06-14 16:08:48 -07:00
Matteo Marescotti
3248f57434
Add support for printing spacer pobs in JSON
2018-06-14 16:08:48 -07:00
Matteo Marescotti
28ef9ab9d1
User option to enable starting spacer from a given level
2018-06-14 16:08:48 -07:00
Matteo Marescotti
ff7c949be8
Fix: call collect_statistics() in virtual_solver
2018-06-14 16:08:48 -07:00
Matteo
65885f7eba
add_constraint API
2018-06-14 16:08:48 -07:00
Matteo
3c7165780c
Extend spacer with callback events
...
Callback events allow the client of spacer to
get events during exection. The events include
new lemmas and unfolding.
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
b51251f394
Move tout under TRACE
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
fd7bcc7afc
Format
2018-06-14 16:08:48 -07:00
Yakir Vizel
5df7a08d1c
A simple version for finding the stride between different indices in a POB
...
This current version is very limited.
It assumes a pre-defined structure (namely, an ADDER).
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
04a778f2fd
Option to enable cube normalization in quic generalizer
2018-06-14 16:08:48 -07:00
Arie Gurfinkel
852e181fed
New quic3 lemma generalizer
2018-06-14 16:08:48 -07:00
