HostedRedmine by Planio

2013-05-26

• 
  Cesare Tinelli Language

  02:20 PM · Created issue

  Bug #180913 (New): inconsistency with :print-success option

  Problem pointed out by David Cok.
  "The SMTLIBv2 standard is clear in its informal text that setting the :print-success option to false suppresses printing 'success' when that would be the result of a command that would respond with ...

2013-03-24

• 
  Cesare Tinelli SMT-LIB

  04:59 AM · Created issue

  Feature #162924 (New): create new web pages for SMT-LIB site

  Create a more modern site.
  Possible web framework to use: http://www.notjustagrid.com/

2013-03-01

• 
  Cesare Tinelli Language

  06:17 PM · Created issue

  Feature #154551 (New): add resource limit command

  Add a command to set some generic resource limit (for each of the next check-sat commands, until changed by a new occurrence of the command).
  See suggestion below by Martin Brain.
  -----------
  Resource limits
  The need is for a rep...
• 
  Cesare Tinelli Theories and Logics

  06:13 PM · Commented on issue

  A similar theory and its decision procedure are described in the paper below. But it is restricted to arrays with integer index.
  Stephan Falke, Carsten Sinz, and Florian Merz:
  A Theory of Arrays with Set and Copy Operations (Extended... Feature #154542: define and add new theory of constructible arrays

  This theory adds to store and select a constructor
  const: B -> (Array A B)
  where const(v) is an array with constant value v.
  The theory's model are limited to those where each array is either constant or the result of finitely...
• 
  Cesare Tinelli This theory adds to store and select a constructor
  const: B -> (Array A B)
  where const(v) is an array with constant value v.
  The theory's model are limited to those where each array is either constant or the result of finitely...

  06:09 PM · Created issue
• 
  Cesare Tinelli Theories and Logics

  05:45 PM · Created issue

  Feature #154522 (New): add a parametrized theory of sets

  A new work group might be needed for this.
  Check first with the community to see how much of a need there is.
  
• 
  Cesare Tinelli Language

  05:40 PM · Created issue

  Feature #154519 (New): Add reset command

  the reset command should force a solver restart.
  Everything is cleared up, including the logic. Operationally, it would be like quitting restarting the solver.
  
• 
  Cesare Tinelli Language

  05:38 PM · Created issue

  Feature #154516 (New): standardize meaning of division by zero in BV logics

  There are some requests to fix the meaning of division by zero.
  What value should we use?
  0 or 1 are good candidates because they occur in every BV sort.
  
• 
  Cesare Tinelli Language

  05:34 PM · Created issue

  Feature #154514 (New): add global declarations

  
  Add the ability to define global declarations/definitions, which can survive a pop.
  Something like
  global-declare-sort
  global-define-sort
  global-declare-fun
  global-define-fun
  These definitions are added to push level 0 regard...
• 
  Cesare Tinelli Language

  05:22 PM · Created issue

  Feature #154503 (New): add get-model command

  Resume discussion of get-model command.
  What is it supposed to return?