mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-27 09:49:23 +00:00
Code Activity
9591 commits 45 branches 52 tags 177 MiB
Commit graph

9591 commits

This branch
This branch
All branches
Author SHA1 Message Date
Arie Gurfinkel
df2e9d8fe2 Make smt_solver::updt_params() commulative 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
9c37bef553 Fix bug in ctp 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
1da002d7b1 scoped params on solver 
solver::push_params() saves current parameters
solver::pop_params() restores previously saved parameters
 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
477ac4a19a Remove dead m_propagate_booleans param 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
40781c0b0c Comment on params used in spacer_context 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
55126692c9 spacer: counterexample to pushing (ctp) 
Enable using fixedpoint.spacer.ctp=true

For each lemma L currently at level k, keep a model M that justifies
why L cannot be pushed to (k+1). L is not pushed while the model M
remains valid.
 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
95d820196b Cleanup 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
68b7966254 Use C++11 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
4e9023b8fe Remove dead code 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
00f870b7ff to_mbp_benchmark(): prints an mbp problem in benchmark format 
currently unused. See comment in spacer_util.c:qe_project for example
usage
 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
bf4c35982f Debug print 2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
efb1f50d00 bind nested variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
d95e167d61 updates to mbqi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
e281f85586 add way to unit test mbp from command line 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
402234757e updates to mbqi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
e8cabdc620 Uninitialized variable 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
054c6196a0 Move spacer qe into spacer_qe namespace 
Attempt to solve compilation issues with GCC and current replication
of qe namespace inside and outside spacer
 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
56bce005a0 virtual_solver: debug print 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
891dcd99c2 Use fact-generating version of mk_unit_resolution() 
fact-using version of mk_unit_resolution() requires the fact to be a
literal. Not sure why this restriction is placed there.
 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
8be03f7c1f spacer_context: skolemize quant vars before renaming 
Skolemization has to be done before renaming, otherwise,
can't guarantee that variable names do not clash
 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
38a45f5482 Fix typo in comment 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
6514741e3f proof-checker: replace match_negated with ast_manager::is_complement 
is_complement matches true and false, while match_negated does not

Necessary to handle uses of true-axiom
 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
9550fd1ec4 proof-checker: handle true-axiom 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
4de58a42fe Update initialization order 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
aeb2f3c4bb factor out inherit_properties 2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
23272f0d2f array support for mbp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
8ffbd5d1e5 model_evaluator: respect array_as_stores option 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
988466705c port array projection to qe_arrays 
ensure it works with multi-dimensional arrays

commit on behalf of Nikolaj
 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
7281616084 model_evaluator: optionally expand arrays as sequence of stores 
commit on behalf of Nikolaj
 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
2f369d8d41 Simplify code using C++11 conventions 2018-06-14 16:08:49 -07:00
Arie Gurfinkel
5a6bd5e782 hypothesis_reducer: worked around propositional literals 
propositional formulas (disjunctions) can appear as literals.  This
makes it tricky to recognize whether a formula is a unit clause when
re-building unit resolution.

Added work-around that identifies whether a formula is a literal based
on its appearance in previous unit resolution step.
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel
b39c532f19 Order of methods in spacer_context.cpp 2018-06-14 16:08:48 -07:00
Nikolaj Bjorner
7931bd1dfc updates to mbqi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel
0fe5e6c2a6 Fix handling of complex literals in hypothesis_reducer 
In Z3, an arbitrary, even propositional, formula can be a literal.

This requires careful handling of restructuring of unit resolution.
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel
d1a7c0ceb0 Remove a print 2018-06-14 16:08:48 -07:00
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