projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Document inferences for strings (#1642)
2018-03-19
Andrew Reynolds
Document inferences for strings (#1642)
commit
|
commitdiff
|
tree
2018-03-13
Mathias Preiner
Use Cryptominisat version 5.0.2 (instead of 4.2.0)...
commit
|
commitdiff
|
tree
2018-03-13
Aina Niemetz
SmtEngine::getModel() is now public. (#1665)
commit
|
commitdiff
|
tree
2018-03-09
Aina Niemetz
Printers are now managed as unique_ptr (fix mem leak...
commit
|
commitdiff
|
tree
2018-03-09
Aina Niemetz
Some minor cleanup in bv::utils. (#1663)
commit
|
commitdiff
|
tree
2018-03-09
Aina Niemetz
Add support for SMT-LIB v2.5 command get-unsat-assumptions...
commit
|
commitdiff
|
tree
2018-03-09
Mathias Preiner
Cleanup Cryptominisat SAT wrapper. (#1652)
commit
|
commitdiff
|
tree
2018-03-09
Mathias Preiner
Fix Travis for unit test compilation errors. (#1651)
commit
|
commitdiff
|
tree
2018-03-07
Mathias Preiner
Make statistics output consistent. (#1647)
commit
|
commitdiff
|
tree
2018-03-06
Andrew Reynolds
Simplify initialization of quantifiers engine (#1641)
commit
|
commitdiff
|
tree
2018-03-06
Andrew Reynolds
Refactor symmetry breaking in datatypes sygus (#1640)
commit
|
commitdiff
|
tree
2018-03-06
Andrew Reynolds
Update semantics for string indexof and replace (#1630)
commit
|
commitdiff
|
tree
2018-03-05
Mathias Preiner
Enable -Wsuggest-override by default. (#1643)
commit
|
commitdiff
|
tree
2018-03-05
Andrew Reynolds
Fix for sampler. (#1639)
commit
|
commitdiff
|
tree
2018-03-05
Aina Niemetz
Add support for check-sat-assuming. (#1637)
commit
|
commitdiff
|
tree
2018-03-05
Aina Niemetz
Add CVC4_PUBLIC keyword to overloads of << for Expr...
commit
|
commitdiff
|
tree
2018-03-05
Aina Niemetz
Add uniform way to serialize containers of Expr to...
commit
|
commitdiff
|
tree
2018-03-02
Andrew Reynolds
Optimization for sygus streaming mode (#1636)
commit
|
commitdiff
|
tree
2018-03-02
Andrew Reynolds
Simplify sygus wrt miniscoping (#1634)
commit
|
commitdiff
|
tree
2018-03-02
Andrew Reynolds
Print candidate rewrites in terms of original grammar...
commit
|
commitdiff
|
tree
2018-03-02
Andrew Reynolds
Create infrastructure for sygus modules (#1632)
commit
|
commitdiff
|
tree
2018-02-28
Aina Niemetz
SmtEngine::getAssignment now returns a vector of assignments...
commit
|
commitdiff
|
tree
2018-02-28
Andrew Reynolds
Minor fixes for rec-fun (#1616)
commit
|
commitdiff
|
tree
2018-02-28
Aina Niemetz
Remove unused code in pushDefineFunRecScop in smt2...
commit
|
commitdiff
|
tree
2018-02-27
Andrew Reynolds
Improve rewriter for string indexof (#1592)
commit
|
commitdiff
|
tree
2018-02-27
Andrew Reynolds
Option to not use partial function semantics for arithmetic...
commit
|
commitdiff
|
tree
2018-02-27
Andrew Reynolds
Improvements to sygus sampling (#1621)
commit
|
commitdiff
|
tree
2018-02-24
Andres Noetzli
Add unit tests for BitVector, minor BV rewrite fix...
commit
|
commitdiff
|
tree
2018-02-23
Aina Niemetz
Split and document bitvector.h. (#1615)
commit
|
commitdiff
|
tree
2018-02-23
Andrew Reynolds
Fix cd-simplification for strings (#1624)
commit
|
commitdiff
|
tree
2018-02-22
Andrew Reynolds
Minor improvements to string rewriter (#1572)
commit
|
commitdiff
|
tree
2018-02-22
Aina Niemetz
Fixed disabling the BV equality slicer for quantifiers...
commit
|
commitdiff
|
tree
2018-02-22
Aina Niemetz
Disable BV equality slicer if not pure QF_BV. (#1619)
commit
|
commitdiff
|
tree
2018-02-20
Aina Niemetz
Improve documentation of bv::utils::isCoreTerm (#1617)
commit
|
commitdiff
|
tree
2018-02-20
Aina Niemetz
Moved and simplified bv::utils::intersect. (#1614)
commit
|
commitdiff
|
tree
2018-02-20
Aina Niemetz
Unrecursified and merged bv::utils::is(Core|Equality...
commit
|
commitdiff
|
tree
2018-02-17
Aina Niemetz
bv::utils::mk(And|Or) Do not return true if size of...
commit
|
commitdiff
|
tree
2018-02-16
Aina Niemetz
Removed bv::utils::mkConjunction (redundant). (#1610)
commit
|
commitdiff
|
tree
2018-02-15
Andrew Reynolds
Fix corner case for rewrite of mult by pow 2 (#1601)
commit
|
commitdiff
|
tree
2018-02-14
Andrew Reynolds
Quantifiers subdirectories (#1608)
commit
|
commitdiff
|
tree
2018-02-14
Aina Niemetz
Provide a uniform way to serialize node containers...
commit
|
commitdiff
|
tree
2018-02-13
Aina Niemetz
Moved (unrecursified) bv::utils::collectVars. (#1602)
commit
|
commitdiff
|
tree
2018-02-13
Aina Niemetz
Skip header for determining top contributors list....
commit
|
commitdiff
|
tree
2018-02-13
Andrew Reynolds
Option to use extended rewriter as a preprocessing...
commit
|
commitdiff
|
tree
2018-02-12
Andrew Reynolds
Minor improvements to sygus sampler (#1598)
commit
|
commitdiff
|
tree
2018-02-11
Aina Niemetz
Move (unrecursified) bv::utils::numNodes to lazy_bitblaster...
commit
|
commitdiff
|
tree
2018-02-11
Andrew Reynolds
More minor improvements to synth-rr (#1597)
commit
|
commitdiff
|
tree
2018-02-10
Aina Niemetz
Move BitVector specific funs from bv::utils to util...
commit
|
commitdiff
|
tree
2018-02-09
Andrew Reynolds
Class to reduce printing of redundant candidate rewrites...
commit
|
commitdiff
|
tree
2018-02-09
Tim King
Replacing an incorrect reference to an injected class...
commit
|
commitdiff
|
tree
2018-02-08
Aina Niemetz
Clean up bv utils (part one). (#1580)
commit
|
commitdiff
|
tree
2018-02-08
Andrew Reynolds
Minor improvements to sygus sampling. (#1577)
commit
|
commitdiff
|
tree
2018-02-08
Tim King
Removing an unused variable. (#1576)
commit
|
commitdiff
|
tree
2018-02-08
Aina Niemetz
Reduce number of Travis builds. (#1578)
commit
|
commitdiff
|
tree
2018-02-07
Aina Niemetz
Use template for bv::utils::mkOr. (#1570)
commit
|
commitdiff
|
tree
2018-02-07
Andrew Reynolds
Add remaining transcendental functions (#1551)
commit
|
commitdiff
|
tree
2018-02-07
Aina Niemetz
Use template for bv::utils::mkAnd. (#1569)
commit
|
commitdiff
|
tree
2018-02-07
Aina Niemetz
Renamed bv::utils::isBVGroundTerm to isBvConstTerm...
commit
|
commitdiff
|
tree
2018-02-07
Aina Niemetz
Split and document theory_bv_utils. (#1566)
commit
|
commitdiff
|
tree
2018-02-07
Mathias Preiner
Use separate shell script for common get-* script parts...
commit
|
commitdiff
|
tree
2018-02-06
Andrew Reynolds
Fix two multiply-by-constant corner cases for bv rewriter...
commit
|
commitdiff
|
tree
2018-02-06
Andrew Reynolds
Fix rewrite for string replace (#1537)
commit
|
commitdiff
|
tree
2018-02-06
Tim King
Using getOperator() directly instead of using -1. CID...
commit
|
commitdiff
|
tree
2018-02-06
Andrew Reynolds
Statically eliminate redundant sygus constructors ...
commit
|
commitdiff
|
tree
2018-02-05
Tim King
Removing references to __gnu_cxx. (#1541)
commit
|
commitdiff
|
tree
2018-02-04
Andrew Reynolds
Sample based on sygus grammar by default (#1558)
commit
|
commitdiff
|
tree
2018-02-03
Andrew Reynolds
Option to use sampling for CEGIS (#1555)
commit
|
commitdiff
|
tree
2018-02-02
Andrew Reynolds
Fix remaining synthesis solution regressions (#1557)
commit
|
commitdiff
|
tree
2018-02-01
Andrew Reynolds
Add interface in sygus to get synthesis solution Nodes...
commit
|
commitdiff
|
tree
2018-02-01
Andrew Reynolds
Use sygus to synthesize/verify rewrite rules (#1547)
commit
|
commitdiff
|
tree
2018-01-30
Andrew Reynolds
Further clean and document datatypes rewriter (#1548)
commit
|
commitdiff
|
tree
2018-01-29
Andrew Reynolds
Generalize explanations for PBE sygus strings based...
commit
|
commitdiff
|
tree
2018-01-28
Andrew Reynolds
Sort children of all commutative operators for sygus...
commit
|
commitdiff
|
tree
2018-01-25
Tim King
Commenting out throw specifiers on SmtEngine. These...
commit
|
commitdiff
|
tree
2018-01-25
Aina Niemetz
Added unit tests for PLUS, NEG, NOT ICs for CBQI BV...
commit
|
commitdiff
|
tree
2018-01-23
Aina Niemetz
Fix MULT handling for CBQI BV. (#1531)
commit
|
commitdiff
|
tree
2018-01-23
Tim King
Commenting out throw specifiers for DeltaRationExceptions...
commit
|
commitdiff
|
tree
2018-01-22
Aina Niemetz
Add previous concat handling for CBQI BV as heuristic...
commit
|
commitdiff
|
tree
2018-01-22
Aina Niemetz
Refactor and fix solveBvLit for CBQI BV. (#1526)
commit
|
commitdiff
|
tree
2018-01-22
Andrew Reynolds
Only push/pop around check-sat if it is associated...
commit
|
commitdiff
|
tree
2018-01-17
Tim King
Removes yet more throw specifiers. Updating the documentatio...
commit
|
commitdiff
|
tree
2018-01-16
Tim King
Removing more miscellaneous throw specifiers. (#1509)
commit
|
commitdiff
|
tree
2018-01-15
Tim King
Removing throw specifiers from Type. (#1511)
commit
|
commitdiff
|
tree
2018-01-12
Andrew Reynolds
Improvements for CBQI BV (#1504)
commit
|
commitdiff
|
tree
2018-01-10
Aina Niemetz
Removed division by constant handling for CBQI BV ...
commit
|
commitdiff
|
tree
2018-01-10
Tim King
Removing throw specifiers from type enumerators. (...
commit
|
commitdiff
|
tree
2018-01-10
Mathias Preiner
Fix linearization for terms where the solve variable...
commit
|
commitdiff
|
tree
2018-01-09
Aina Niemetz
Reorganized bitvector.h. (#1505)
commit
|
commitdiff
|
tree
2018-01-09
Aina Niemetz
Fix output of --trace=help. (#1500)
commit
|
commitdiff
|
tree
2018-01-09
Tim King
Removing more miscellaneous throw specifiers. (#1488)
commit
|
commitdiff
|
tree
2018-01-09
Aina Niemetz
Add bv util mkConst(unsigned, Integer&). (#1499)
commit
|
commitdiff
|
tree
2018-01-09
Aina Niemetz
Added division by constant handling for CBQI BV. (...
commit
|
commitdiff
|
tree
2018-01-08
Aina Niemetz
Remove portfolio option from builds. (#1496)
commit
|
commitdiff
|
tree
2018-01-08
Andrew Reynolds
Improvements to quant+BV/Bool variable elimination...
commit
|
commitdiff
|
tree
2018-01-08
Tim King
Re-ordering field initialization in QuantInfo to remove...
commit
|
commitdiff
|
tree
2018-01-08
Tim King
Removes RationalFromDoubleException. Replaces this...
commit
|
commitdiff
|
tree
2018-01-06
Mathias Preiner
Add special {SGE,SGT,NE}_UDIV1 side conditions for...
commit
|
commitdiff
|
tree
2018-01-06
Mathias Preiner
Use simpler EQUAL SCs for LSHR0, LSHR1, ASHR0, AHSR1...
commit
|
commitdiff
|
tree
2018-01-05
Mathias Preiner
Add UGT/SGT side conditions for AND/OR + other fixes...
commit
|
commitdiff
|
tree
2018-01-05
Mathias Preiner
Add side conditions for inequalities of SHL. (#1472)
commit
|
commitdiff
|
tree
next