projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5062257) | patch
Factors out the QF_LRA decision procedure from TheoryArith and puts this into its...
authorTim King <taking@cs.nyu.edu>
Fri, 29 Oct 2010 00:45:10 +0000 (00:45 +0000)
committerTim King <taking@cs.nyu.edu>
Fri, 29 Oct 2010 00:45:10 +0000 (00:45 +0000)
commit7d4a5842ea4f53fe2e05f336c9342db9b94a31f1
tree5a03a7191c7ab370e91dc4205305dc7f81df7073tree
parent50622574025f55417be020f30a4787714977ddd1commit | diff
Factors out the QF_LRA decision procedure from TheoryArith and puts this into its own class SimplexDecisionProcedure. Implements about 1/2 of the pivoting rule from Alberto's thesis (section2.5.3).
src/theory/arith/Makefile.am diff | blob | history
src/theory/arith/simplex.cpp [new file with mode: 0644] blob
src/theory/arith/simplex.h [new file with mode: 0644] blob
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history