projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 349deb0) | patch
Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false...
authorajreynol <andrew.j.reynolds@gmail.com>
Sun, 26 Apr 2015 17:26:21 +0000 (19:26 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Sun, 26 Apr 2015 17:26:21 +0000 (19:26 +0200)
commitf07e8a3f06feb789692ede8ad9d25a2e049af769
treebdeb79262056c70c6b5125ed11a392a4fa1864f7tree
parent349deb0522c4602b740d96f6a688b644dd84c64fcommit | diff
Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions.
14 files changed:
src/theory/quantifiers/first_order_model.cpp diff | blob | history
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/quantifiers/fun_def_process.cpp diff | blob | history
src/theory/quantifiers/fun_def_process.h diff | blob | history
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers/inst_match.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/rep_set.cpp diff | blob | history
src/theory/rep_set.h diff | blob | history
src/theory/theory_model.cpp diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/fib-core.smt2 [new file with mode: 0755] blob
test/regress/regress0/fmf/fore19-exp2-core.smt2 [new file with mode: 0755] blob
test/regress/regress0/fmf/with-ind-104-core.smt2 [new file with mode: 0755] blob