cvc5.git
2020-02-26 Andrew ReynoldsBasic support for regular expression complement (#3437)
2020-02-26 Andrew ReynoldsRefactor type ascriptions in the parser (#3825)
2020-02-26 Andrew ReynoldsMinor improvement to ParseOp (#3808)
2020-02-26 Andrew ReynoldsUse default consts when not using any const during...
2020-02-26 Andrew ReynoldsFix node arity issue in reduction of int2bv (#3777)
2020-02-26 Andrew ReynoldsMove equivalence class info to its own file in strings...
2020-02-26 Andrew ReynoldsSupport for witnessing choice in models (#3781)
2020-02-26 Andres NoetzliRemove portfolio leftovers (#3821)
2020-02-26 Andrew ReynoldsMinor cleaning of smt2 parser (#3823)
2020-02-26 Andrew ReynoldsEmbed mkAssociative utilities within the API. (#3801)
2020-02-25 mudathirmahgoubSets & Relations Java example (#3816)
2020-02-25 mudathirmahgoubSets & Relations Java example (#3816)
2020-02-25 yoni206remove redundant includes (#3815)
2020-02-25 yoni206bv_to_int preprocessing pass
2020-02-24 Andrew ReynoldsFixes for quantifiers documentation (#3811)
2020-02-24 Andrew ReynoldsUtilities for words (#3797)
2020-02-24 Andrew ReynoldsConvert parser input interface to api::Term (#3809)
2020-02-24 Abdalrhman... Fix bugs related to printing Sygus commands (#3804)
2020-02-24 Andrew ReynoldsAdd missing functions to new C++ API (#3769)
2020-02-24 Andres NoetzliMake lambda rewriter more robust (#3806)
2020-02-23 Andrew ReynoldsMinor refactoring of equality notifications (#3798)
2020-02-22 Alex OzdemirRIP th_lra.plf (#3796)
2020-02-22 Andrew Reynolds Move check memberships to reg exp solver (#3793)
2020-02-22 Andrew ReynoldsMove cardinality inference scheme to base solver in...
2020-02-22 makaimannDump boolean propagations and conflicts for decision...
2020-02-22 Alex OzdemirSwitch to th_lira.plf (#3741)
2020-02-21 Aina NiemetzNew C++ API: Remove TOTAL kinds. (#3794)
2020-02-21 Andrew ReynoldsSimple changes towards unicode string standard (#3791)
2020-02-21 Andrew V. JonesAdding checks to the validation of 'bv-sat-solver'...
2020-02-21 Andrew ReynoldsSplit extended functions solver in strings (#3768)
2020-02-21 Alex OzdemirRemove IntReal tightening axioms from th_lira.plf ...
2020-02-20 Andrew ReynoldsRemove front-end support for Chain (#3767)
2020-02-20 Andres NoetzliRemove unused code (#3782)
2020-02-20 Andrew ReynoldsMinor removals (#3786)
2020-02-20 Andres NoetzliRemove parser from bindings (#3779)
2020-02-20 Mathias Preinerresource manager: Add statistic for every resource...
2020-02-19 Andrew ReynoldsFix symmetry breaking for multiple sygus types (#3775)
2020-02-19 makaimannAdd Python bindings using Cython -- see below for more...
2020-02-19 Andrew ReynoldsDelay enumerative instantiation if theory engine does...
2020-02-19 Andrew ReynoldsChange Record to shared_ptr (#3778)
2020-02-19 Andrew ReynoldsFix approximate bounds for transcendental functions...
2020-02-19 makaimannChange datatype selector/constructor/tester to terms...
2020-02-18 Andrew ReynoldsAdd missing kinds for the new API (#3757)
2020-02-17 Andrew ReynoldsOption to limit the number of rounds of enumerative...
2020-02-17 Andrew Reynolds Fix soundness bug in reduction of integer div/mod...
2020-02-17 Haniel BarbosaUsing ParseOp in TPTP (#3764)
2020-02-17 Abdalrhman... Support dumping Sygus commands. (#3763)
2020-02-16 Andrew ReynoldsFix simple issue with cache (#3762)
2020-02-16 Andrew ReynoldsAdd temporary global API conversion utilities. (#3759)
2020-02-16 Andres NoetzliActivate reverse variant of F-Split inference (#3745)
2020-02-16 Andrew ReynoldsDisable regression (#3761)
2020-02-15 Andrew ReynoldsMove proxy variables to InferenceManager in strings...
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754)
2020-02-14 Andrew ReynoldsUpdate sygus v1 parser to use ParseOp utility (#3756)
2020-02-14 Haniel BarbosaForcing rewrite pass rather than asserting if formula...
2020-02-13 Andrew ReynoldsConst input for sygus print callback (#3755)
2020-02-13 Andres Noetzli[Python] Properly destroy CVC4 object (#3753)
2020-02-12 Andres NoetzliRename Java package to edu.stanford.CVC4 (#3752)
2020-02-12 Andrew ReynoldsEnsure ext rewrites for associative ops dont throw...
2020-02-12 Mathias Preinerrun_regression: Distinguish between timeout and failure...
2020-02-12 Andrew ReynoldsFix non-linear equality solving that involves mixed...
2020-02-11 Mathias Preinercmake: Remove unused ENABLE_OPTIMIZED option. (#3749)
2020-02-11 Andrew ReynoldsFix term simplification based on entailment in quantifi...
2020-02-11 Mathias PreinerUpdate issue templates
2020-02-11 Andres NoetzliRemove `--strings-binary-csp` option (#3743)
2020-02-11 Andres NoetzliRefactor `CoreSolver::processSimpleNEq()` (#3736)
2020-02-11 Andrew ReynoldsUse example evaluation cache instead of sygus PBE ...
2020-02-11 Alex OzdemirImplement LFSCArithProof::equalityType. (#3740)
2020-02-10 Alex OzdemirAdd function for tightening literals (#3732)
2020-02-10 Mathias Preinercmake: Use ld.gold if available for faster link times...
2020-02-10 Alex OzdemirAdd more IntReal predicates (#3731)
2020-02-08 Andrew ReynoldsFix rewrite rules sat regressions (#3734)
2020-02-08 Andres NoetzliMake "unknown" non-critical for unsat cores check ...
2020-02-08 Andrew ReynoldsSplit strings finite model finding strategy (#3727)
2020-02-08 Andrew ReynoldsSplit core solver from the theory of strings (#3713)
2020-02-08 Andrew ReynoldsInterface for example evaluation cache utilities (...
2020-02-07 mudathirmahgoubUniveset Cardinality constraints for infinite types...
2020-02-07 Andrew ReynoldsRefactor check-model handling in SmtEngine (#3723)
2020-02-07 Alex OzdemirPropagate expected types through UF arguments (#3717)
2020-02-07 Alex OzdemirAdd `ArithProof::{printInteger,getLfscFunction}` (...
2020-02-07 Andrew ReynoldsStatistics for fast enumerator (#3699)
2020-02-07 Andrew ReynoldsExample evaluation cache utility (#3698)
2020-02-07 Andrew ReynoldsFix exact sqrt (#3721)
2020-02-06 Andrew ReynoldsGeneralize containsQuantifiers to hasClosure (#3722)
2020-02-05 Andrew ReynoldsFix QF_NIA smt comp script (#3715)
2020-02-04 mudathirmahgoubUpdate INSTALL.md (#3714)
2020-02-04 Alex OzdemirArticulate proof-related debug statements in arith...
2020-02-04 Aina Niemetz--fp-exp: Better warning message. (#3709)
2020-02-04 Mathias PreinerFix header installation on MacOS. (#3660)
2020-02-04 Andrew ReynoldsSplit base solver from the theory of strings (#3680)
2020-02-04 Andres NoetzliRevert semantic change from refactoring (#3711)
2020-02-04 Alex OzdemirRegression tests for arithmetic proofs. (#3701)
2020-02-04 Aina NiemetzIncrease regression test time limit to 1200s. (#3704)
2020-02-03 Clark BarrettFix corner case - might need to REWRITE_AGAIN (#3706)
2020-02-03 Andrew ReynoldsUtility function for getting component types (#3703)
2020-02-03 Andrew ReynoldsMinor fixes to regressions (#3702)
2020-02-03 mudathirmahgoubFix cardinality of uninterpreted types when univset...
2020-02-03 Andrew ReynoldsSplit on model values when repaired model from non...
2020-02-03 Andrew ReynoldsFix invariant template inference for trivially infeasib...
2020-02-03 Andrew ReynoldsFix corner case of empty domains in bounded fmf (#3690)
next