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
Arie Gurfinkel
9cdb63ae4a
Handle conversion of quantified lemma to quantifier free
...
When a cube is updated, a lemma might loose all of its quantified
variables. In this case, it is effectively quantifier free
and might be a version of an already existing lemma.
For that reason, we convert it to quantifier free lemma when
this happens.
2018-06-14 16:08:48 -07:00
Yakir Vizel
23a8e59493
Initial commit of QGen
...
Controlled by fixedpoint.spacer.use_quanti_generalizer
measure cumulative time, number of invocations, and number of failed
SMT calls
Relaxing equality in a pattern: if a variable equals a numeral, relax with GE
pob::get_skolems() returns all skolems that might appear in the pob.
New skolems must be added above the largest index in that map,
even if they are not used in the pob itself.
pattern generalization should be done before the pattern is skolemized and
added into the new cube.
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
a1efb88318
Semantic matcher
...
Extends matcher with rewrites based on semantics of arithmetic operations
Like matcher, but uses arithmetic and logic rewrites to try to
get a semantic match.
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
7dee36358d
Allow bool_ind_generalizer to skip non-array literals
...
Currently a hack to skip generalizing some literals.
Used together with quic generalizer to remove all array terms if possible
before quic generalization
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
46fb0d928a
Fix in spacer_term_graph
2018-06-14 16:08:47 -07:00
Yakir Vizel
068b77d43a
Normalizing LE and GE with constants
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
0c1ef7155a
Option to rewrite expression in term_graph
...
Rewrite expressions to minimize uses of constants 0 and 1
Currently disabled due to interaction with quic
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
ecf9c629b0
Fix binding handling for quantifier free lemmas
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
a8318b8822
Fix lemma::has_binding()
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
ec179da0fa
API to get num of free variables in a pob
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
05e876d684
Fix n-arry applications in spacer_term_graph
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
7b82ec1bee
Attempt bug fix
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
981e521b18
Cleanup lemma definition
...
exposes a potential bug. See comments in code.
2018-06-14 16:08:47 -07:00
Yakir Vizel
f51c07adf6
Moving skolems to lemma
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
ea73acef45
Implements mk_num_pat
...
Abstracts interpreted numeric constants with variables in a ground expression
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
9bc11b2122
Wire term graph into eq_generalizer
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
09d54c10a6
Wire term graph into spacer normalizer
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
be77b1de39
Improve interface of term_graph
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
6407ec8725
spacer_term_graph: an egraph of terms
...
Used to determine and factor out equalities
2018-06-14 16:08:47 -07:00
Arie Gurfinkel
088bd3ed8e
Fix compiler warning
2018-06-14 16:08:47 -07:00
Bernhard Gleiss
25fad153d1
added option fixedpoint.spacer.iuc.debug_proof to debug proof which is used for generation of iuc
2018-06-14 16:08:47 -07:00
Bernhard Gleiss
c3a66217e1
improved options for IUC computation
2018-06-14 16:08:47 -07:00
Bernhard Gleiss
370667722d
New option fixedpoint.spacer.print_farkas_stats
...
Prints the number of Farkas lemmas in each proof
2018-06-14 16:08:47 -07:00
