projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 95992fb) | patch
Extend counterexample-guided instantiation to extended theory of Int/Real, mixed...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 26 Oct 2015 10:26:13 +0000 (11:26 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 26 Oct 2015 10:26:22 +0000 (11:26 +0100)
commitaaf1bbbdc6e42910e07db64441885ee3476d86df
treea6abf77b1b404e8183a44c78f733a0c93f2213fetree
parent95992fb5e9fb971f2319e1302b83ac85098e0438commit | diff
Extend counterexample-guided instantiation to extended theory of Int/Real, mixed Int/Real. Bug fixes. Updates to quantifiers rewriter.
15 files changed:
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/ceg_instantiator.h diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect [deleted file] blob | history
test/regress/regress0/quantifiers/bug291.smt2 diff | blob | history
test/regress/regress0/quantifiers/bug291.smt2.expect diff | blob | history
test/regress/regress0/quantifiers/floor.smt2 [new file with mode: 0755] blob
test/regress/regress0/quantifiers/is-int.smt2 [new file with mode: 0755] blob