Solving Quantified Bit-Vectors Using Invertibility Conditions

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli

This site provides our paper Solving Quantified Bit-Vectors Using Invertibility Conditions and related material at CAV 2018.

An extended version of our paper at CAV 2018 can be found below.

All materials to reproduce the experimental evaluation in our paper can be found below.

Downloads

• Paper at CAV 2018
• Extended version of our paper at CAV 2018
• README for the artifact
• Artifact [tar.xz] as submitted to the artifact evaluation at CAV 2018
• Benchmarks [tar.gz]
  set of 160 benchmarks in the syntax-guided synthesis format (.sy) as submitted to SYGUS COMP 2018
• CVC4 Binary [tar.xz]
  implementing configurations (with options)
  • cegqi_b: --no-cond-rewrite-quant --cbqi-bv-ineq=eq-boundary --global-negate --no-cbqi-innermost --ext-rew-prep
  • cegqi_k: --no-cond-rewrite-quant --cbqi-bv-ineq=keep --global-negate --no-cbqi-innermost --ext-rew-prep
  • cegqi_m: --no-cond-rewrite-quant --no-cbqi-bv --global-negate --no-cbqi-innermost --ext-rew-prep
  • cegqi_s: --no-cond-rewrite-quant --cbqi-bv-ineq=eq-slack --global-negate --no-cbqi-innermost --ext-rew-prep