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
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
