upscale-project / pono Goto Github PK

Pono: A flexible and extensible SMT-based model checker

License: Other

C++ 89.31% Shell 1.11% Makefile 0.11% CMake 1.32% Python 1.78% Lex 0.46% Yacc 3.64% Cython 2.28%

pono's Introduction

Pono: A Flexible and Extensible SMT-Based Model Checker

Pono is a performant, adaptable, and extensible SMT-based model checker implemented in C++. It leverages Smt-Switch, a generic C++ API for SMT solving. Pono was developed as the next generation of CoSA and thus was originally named cosa2.

Pono is the Hawaiian word for proper, correct, or goodness. It is often used colloquially in the moral sense of "goodness" or "rightness," but also refers to "proper procedure" or "correctness." We use the word for multiple meanings. Our goal is that Pono can be a useful tool for people to verify the correctness of systems, which is surely the right thing to do.

Publications

Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark W. Barrett: Pono: A Flexible and Extensible SMT-Based Model Checker. CAV 2021.
- Evaluated software artifact.
Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, Clark W. Barrett: Smt-Switch: A Solver-Agnostic C++ API for SMT Solving. SAT 2021.
Makai Mann: Augmenting transition systems for scalable symbolic model checking. PhD thesis, Stanford University, 2021.

Awards

Pono was awarded the Oski Award under its original name cosa2 at HWMCC'19 for solving the largest number of benchmarks overall.

Setup

[optional] Install bison and flex
- If you don't have bison and flex installed globally, run ./contrib/setup-bison.sh and ./contrib/setup-flex.sh
- Even if you do have bison, you might get errors about not being able to load -ly. In such a case, run the bison setup script.
Run ./contrib/setup-smt-switch.sh -- it will build smt-switch with Bitwuzla
- [optional] to build with MathSAT (required for interpolant-based model checking) you need to obtain the libraries yourself
  - note that MathSAT is under a custom non-BSD compliant license and you must assume all responsibility for meeting the conditions
  - download the solver from https://mathsat.fbk.eu/download.html, unpack it and rename the directory to ./deps/mathsat
  - then add the --with-msat flag to the setup-smt-switch.sh command.
Run ./contrib/setup-btor2tools.sh.
Run ./configure.sh.
- if building with mathsat, also include --with-msat as an option to configure.sh
Run cd build.
Run make.

Dependencies

Please see the README of smt-switch for required dependencies.
Note to Arch Linux users: building Pono will fail if the static library of GMP, which is required by cvc5, is not installed on your system. You can fix it by installing libgmp-static from AUR.

Profiling

We link against the gperftools library to generate profiling data. To enable profiling, run ./configure.sh with flag --with-profiling and recompile Pono by running make in the build directory. This assumes that you have installed the gperftools library before, e.g., on Ubuntu, run sudo apt-get install google-perftools libgoogle-perftools-dev.

To profile, run ./pono --profiling-log=<log-file> ... where <log-file> is the path to a file where profiling data is written. After normal or abnormal (e.g. via sending a signal) termination of Pono, the collected profile data can be analyzed by running, e.g., google-pprof --text ./pono <log-file> to produce a textual profile. See man google-pprof for further options.

In general, see https://github.com/gperftools/gperftools/tree/master/docs for further information about gperftools.

gperftools is licensed under a BSD 3-clause license, see https://github.com/gperftools/gperftools/blob/master/COPYING.

Existing code

Transition Systems

There are two Transition System interfaces:

FunctionalTransitionSystem in fts.*
TransitionSystem in rts.*

Smt-Switch

Smt-switch is a C++ solver-agnostic API for SMT solvers. The main thing to remember is that everything is a pointer. Objects might be "typedef-ed" with using statements, but they're still shared_ptrs. Thus, when using a solver or a term, you need to use -> accesses.

For more information, see the example usage in the smt-switch tests. Other useful files to visit include:

smt-switch/include/solver.h: this is the main interface you will be using
smt-switch/include/ops.h: this contains all the ops you might need
- Note: create indexed ops like Op(Extract, 7, 4)

Python bindings

To build the pono python bindings, first make sure that you have Cython version >= 0.29 installed. Then ensure that smt-switch and its python bindings are installed. Finally, you can configure with ./configure.sh --python and then build normally. The sequence of commands would be as follows:

# Optional recommended step: start a python virtualenv
# If you install in the virtualenv, you will need to activate it each time before using pono
# and deactivate the virtualenv with: deactivate
python3 -m venv env
source ./env/bin/activate
pip install Cython==0.29 pytest
./contrib/setup-smt-switch.sh --python
./contrib/setup-btor2tools.sh
pip install -e ./deps/smt-switch/build/python
./configure.sh --python
cd build
make -j4
pip install -e ./python
cd ../
# Test the bindings
pytest ./tests

Generating BTOR2 from Verilog

The best tool for creating BTOR2 from Verilog is Yosys. Yosys has an excellent manual here. You can also run yosys interactively by running yosys with no arguments. Then you can view help messages for each command with: help <command>. Running help with no arguments lists all commands.

A particularly useful command if you're having trouble is show, which can show the current state of the circuit in Yosys.

Yosys Quick Start

Below is an example file with comments explaining each command that produces a BTOR2 file for ./samples/counter-false.v. This should be enough for most use cases.

Once you have yosys installed, copy the text below into gen-btor.ys in the top-level of this repository. Then, running yosys -s gen-btor.ys will produce the BTOR2 file.

# read in the file(s) -- there can be multiple
# whitespace separated files, and you can
# escape new lines if necessary
read -formal ./samples/counter-false.v;

# prep does a conservative elaboration
# of the top module provided
prep -top counter;

# this command just does a sanity check
# of the hierarchy
hierarchy -check;

# If an assumption is flopped, you might
# see strange behavior at the last state
# (because the clock hasn't toggled)
# this command ensures that assumptions
# hold at every state
chformal -assume -early;

# this processes memories
# nomap means it will keep them as arrays
memory -nomap;

# flatten the design hierarchy
flatten;

# (optional) uncomment and set values to simulate reset signal
# use -resetn for an active low pin
# -n configures the number of cycles to simulate
# -rstlen configures how long the reset is active (recommended to keep it active for the whole simulation)
# -w tells it to write back the final state of the simulation as the initial state in the btor2 file
# another useful option is -zinit which zero initializes any uninitialized state
# sim -clock <clockpin> -reset <resetpin> -n <number of cycles> -rstlen <number of cycles> -w <top_module>

# (optional) use an "explicit" clock
# e.g. every state is a half cycle of the
# fastest clock
# use this option if you see errors that
# refer to "adff" or asynchronous components
# IMPORTANT NOTE: the clocks are not
# automatically toggled if you use this option
# clk2fflogic;

# This turns all undriven signals into
# inputs
setundef -undriven -expose;

# This writes to a file in BTOR2 format
write_btor counter-false.btor2

pono's People

Contributors

Stargazers

Watchers

pono's Issues

Use constant references for iteration

When iterating over a data structure, we should use const auto & if the variable can be const.

Pono outputs longer than expected witness

I have the following chisel code

class DivisionByZeroIsEq(to: Int) extends Module {
  val a = IO(Input(UInt(2.W)))
  val b = IO(Input(UInt(2.W)))
  val d = a / b
  assume(b === 0.U)
  assert(d === to.U)
}

Which compiles to the following btor2 output:

1 sort bitvec 1
2 input 1 reset
3 sort bitvec 2
4 input 3 a ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 61:13]
5 input 3 b ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 62:13]
6 input 3 d_invalid ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 63:13]
; _resetCount.init
7 zero 1
8 state 1 _resetCount
9 init 1 8 7
10 zero 3
11 eq 1 5 10 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 63:13]
12 udiv 3 4 5
13 ite 3 11 6 12 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 63:13]
14 zero 1
15 uext 3 14 1
16 eq 1 5 15 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 64:12]
17 not 1 2 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 64:9]
18 not 1 16 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 64:9]
19 zero 1
20 uext 3 19 1
21 eq 1 13 20 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 65:12]
22 not 1 21 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 65:9]
23 one 1
24 ugte 1 8 23
25 not 1 24
26 implies 1 17 16
27 constraint 26 ; assume @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 64:9]
28 implies 1 17 21
29 not 1 28
30 bad 29 ; assert @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 65:9]
31 implies 1 25 2
32 constraint 31 ; _resetActive
; _resetCount.next
33 uext 3 8 1
34 one 1
35 uext 3 34 1
36 add 3 33 35
37 slice 1 36 0 0
38 ite 1 25 37 8
39 next 1 8 38

The output of pono gives a witness of length 2:

$ pono -e bmc -k 2 --vcd ignore.vcd DivisionByZeroIsEq.btor
sat
b0
#0
0 0 _resetCount@0
@0
0 1 reset@0
1 00 a@0
2 00 b@0
3 00 d_invalid@0
@1
0 0 reset@1
1 11 a@1
2 00 b@1
3 10 d_invalid@1
@2
0 1 reset@2
1 00 a@2
2 00 b@2
3 00 d_invalid@2
.

Whereas btormc takes only a single step:

$ btormc --kmax 1 DivisionByZeroIsEq.btor 
b0
@0
0 1 reset@0
1 00 a@0
2 00 b@0
3 00 d_invalid@0
@1
0 0 reset@1
1 00 a@1
2 00 b@1
3 10 d_invalid@1
.

Pono really should be failing the bounded model check in a single step.

Look into performance issues with large unrolls

Cosa2 takes 4m to unroll to bound 26,000 on my desktop, and btormc takes only 9s to unroll and solve.

example.tar.gz

UNKNOWN instead of SAT for BMC benchmark

I have a benchmark that returns a witness with btormc -kmax 25 but returns unknown with cosa2 -k 25 -e bmc.

First, I would have expected -e bmc to only return sat or unsat, never unknown. Am I missing something?

Second, is this a bug? Would there be value in making this benchmark available? (Would require some work on my side to remove some secret stuff, and I could only provide it to individual persons, not publish it here.)

Make better interface for TS abstraction

Rethink interface for modifying transition system. The current features are a bit heavy handed and dangerous:

Swap Relational and Functional Transition system relationship

There are often cases where want to take a functional transition system but not a relational transition system. This is difficult with the current inheritance relationship.

Look into infrequent errors in interpolation

Mentioned here: #53

It's possible this is in MathSAT in which case there's not much we can do. But we should be sure that's the case.

Destruct pointers in Cython bindings

Need to implement __dealloc__ to delete pointers used in the Cython bindings.

Build failed when bash > 5.2

Maybe should update smt-switch version

https://github.com/cvc5/cvc5/blob/86fe72f6d25023387dbc76be9a6c97d4d27e41d3/src/expr/mkmetakind#L19

Possible enhancement: Check for weaker interpolants

Attached is a simple example that interpolant-based model checking diverges on. It turns out that the generated interpolants are too strong and keep getting expanded with constant values. However, the first interpolant actually contained the "right" interpolant as one of its conjuncts. If we had detected that a subformula was itself an interpolant, this would not happen.

itp_fail_test.tar.gz

tests/python/test_encoders.py AttributeError

It doesn't look like tests/python/test_encoders.py is being run on travis since it's the build is not configured with coreir. However, even if it is being run, it will give a false positive because of #97 (since the travis script runs the test from the project root directory).

When I run the test with the correct path, I get:

______________________________________________________________ test_coreir[create_cvc4_solver] _______________________________________________________________

create_solver = <built-in function create_cvc4_solver>

    @pytest.mark.skipif(not COREIR_AVAILABLE, reason="Requires coreir python bindings")
    @pytest.mark.parametrize("create_solver", ss.solvers.values())
    def test_coreir(create_solver):
        file_dir = Path(os.path.dirname(__file__))
        coreir_inputs_directory = file_dir / Path("../encoders/inputs/coreir")
        for f in coreir_inputs_directory.glob("*.json"):
            print("Encoding:", f)
            context = coreir.Context()
            top_mod = context.load_from_file(str(f))

            solver = create_solver(False)
            rts = c.RelationalTransitionSystem(solver)
            ce = c.CoreIREncoder(top_mod, rts)
            t = solver.make_term(True)
>           assert ce.trans != t, "Expecting a non-empty transition relation"
E           AttributeError: 'pono.CoreIREncoder' object has no attribute 'trans'

tests/python/test_encoders.py:29: AttributeError

Is there a different API I should be using instead of .trans?

MBIC3 issue

Hi Makai, this is actually not related to anything I'm working on, maybe not an issue at all, but just to let you know currently MBIC3 seems to be abnormal: producing invariants that are checked to be not inductive.

You can try with the anderson.2.prop1-func-interl.btor2 in the sample.

This is what I got on my end, by running: pono -e mbic3 -v 3 --check-invar anderson.2.prop1-func-interl.btor2

Propagation phase at frame 5
INVARCHECK: init |= inv...OK
INVARCHECK: inv & trans |= inv'...FAIL
INVARCHECK: inv |= prop...OK
Invariant Check FAILED
unknown
b0

Failure for a small btor2 case

Here is a btor2 file within 42 lines. We have verified the syntactic correctness of this case with btro2tools/catbtor.

1 sort bitvec 1
2 sort bitvec 5
3 consth 2 10
4 consth 2 11
5 mul 2 3 4
6 consth 2 01
7 const 2 01001
8 sll 2 6 7
9 smulo 1 5 8
10 sort bitvec 3
11 const 10 110
12 sort bitvec 2
13 one 12
14 state 1 bv0_1
15 concat 10 13 14
16 ror 10 11 15
17 init 1 14 9
18 sort bitvec 8
19 constd 18 -111
20 const 18 01000110
21 xor 18 19 20
22 slice 1 21 3 3
23 next 1 14 22
24 state 10 bv1_3
25 init 10 24 16
26 xnor 10 24 24
27 not 10 26
28 sra 10 27 24
29 next 10 24 28
30 sort bitvec 6
31 sort array 1 30
32 state 31 arr0_1_6
33 input 30
34 write 31 32 14 33
35 sgte 1 24 24
36 mul 30 33 33
37 write 31 34 35 36
38 sub 30 33 33
39 mul 30 38 33
40 write 31 37 35 39
41 next 31 32 40
42 bad 14

Checking this file with command "./pono -e ic3ia -k 1000000" produces the following error message:

      _[boolector] boolector_slice: 'upper' must not be < 'lower'
      error
      b0_

If I modify the operator in line 16 from "ror" to "add", Pono produces the result normally:

      _sat
      b0_

May I ask is it a bug in Pono or the usage of "ror" operator is wrong in this case?

Version of pono commit: 8b2a946

Consider changing logger implementation

A few reasons to change the logger implementation:

it seems like the logger evaluates all the arguments regardless of the verbosity (e.g. even if it doesn't print it). This means the to_string for large terms could be called all the time even at low verbosity.
I believe it is the only part of the codebase that uses C++17

Could consider looking into a stream based one -- maybe that would help. A macro could also work, but we do want to be able to change the verbosity dynamically so it would have to take an argument.

Implement Cone of Influence reduction

Special unroller for functional unrolling

Encoder directly from Yosys RTLIL

It could be very nice to have encoder directly from Yosys to a transition system instead of going through BTOR2. This is not currently a priority, but it would give us more control over the encoding.

Handle multi-property monitors better

If a property contains next states or inputs, then a property monitor state variable is introduced. In the case where multiple properties are checked on the same transition system, this could pollute the system with too many extra state variables. We should figure out a better way to handle this.

Related to #104

Revisit input formalism

There are two world-views for how inputs should behave in a transition system:

they should be state variables with no update constraints
they should be affiliated only with the transition and thus not be involved in any formula referring to a set of states (only sets of pairs of states -- e.g. the transition relation)

Option 1 makes more sense in hardware and less sense for relational systems. However, adhering to closely to 2 can also cause problems (see #261). We should discuss how to best unify these ideas for different inputs to Pono.

How to use `pono` correctly with `clk2fflogic`?

I'm attempting to verify a synchronous hardware design, written in Verilog, and expressed in BTOR2 using Yosys. I've followed the guidance in the 'Generating BTOR2 from Verilog' section of the README.

The issue that I'm having is that my design is producing $aldff cells in Yosys. I used the clk2fflogic pass to eliminate these cells and produced syntactically valid BTOR2. However, I'm not getting the results I expect from executing the BTOR using pono.

I'm wondering if someone could clarify the meaning of the "IMPORTANT NOTE" in the README above the clk2fflogic pass:

# (optional) use an "explicit" clock
# e.g. every state is a half cycle of the
# fastest clock
# use this option if you see errors that
# refer to "adff" or asynchronous components
# IMPORTANT NOTE: the clocks are not
# automatically toggled if you use this option
# clk2fflogic;

Does this mean that even if I point pono at the appropriate symbol using the -c flag, the bounded model checking will not correctly toggle the input on each iteration?

Thanks in advance for the help, I really appreciate it!

Crash when extracting counterexample trace

Attached are the Verilog and Btor2 that will trigger crash (segmentation fault) when extracting counter-example trace in Prover::witness at Term r = solver_->get_value(vi);.

I think it is on m1.l15.mshr.ld_homeid (which is an array) at time 0. I'm sorry but I don't think I'm knowledgeable enough to tell what exactly causes the problem.

Thanks!

crash.zip

Heisenbug with smt-switch boolector backend

In certain (supposedly rare cases) running BMC with the boolector backend will return an incorrect result. Reproducible on this branch: https://github.com/upscale-project/cosa2/tree/debugging. Small changes, such as adding/removing a print statement that just prints an arbitrary string, will change the result.

The bug might be in https://github.com/makaimann/smt-switch or in boolector.

support for Arithmetic Theories

Improve infrastructure for transferring between solvers

It is often a headache to maintain formulas over multiple solvers. This can be seen with complicated code in some areas, for example:

https://github.com/upscale-project/pono/blob/a2d993cc8c3a948150586ce014066f479045a74a/engines/ic3ia.cpp#L156
This case occurs with IC3IA because the UF abstraction symbols already exist in the solver but are not in the TermTranslator's cache so they can't be looked up https://github.com/upscale-project/pono/blob/a2d993cc8c3a948150586ce014066f479045a74a/engines/ceg_prophecy_arrays.cpp#L165

We need a better way to manage multiple solvers.

simple_alu.py - RuntimeError: BoolectorSolver::make_sort

How can I try to fix this?
Fresh build of pono with everything except CoreIR.
--with-msat:

Traceback (most recent call last):
  File "/home/xxx/xxx/xxx/pono/examples/python-api/simple_alu.py", line 158, in <module>
    k_induction_attempt()
  File "/home/xxx/xxx/xxx/pono/examples/python-api/simple_alu.py", line 61, in k_induction_attempt
    prop = build_simple_alu_fts(s)
  File "/home/xxx/job/xxx/pono/examples/python-api/simple_alu.py", line 16, in build_simple_alu_fts
    fts = pono.FunctionalTransitionSystem(s)
  File "pono_imp.pxi", line 57, in pono.__AbstractTransitionSystem.__cinit__
RuntimeError: BoolectorSolver::make_sort

Process finished with exit code 1

Without msat:

============== Running k-induction ==============
INIT
	(bvand (bvnot cfg) (ite (= spec_res imp_res) #b1 #b0))
TRANS
	(and (= spec_res.next (bvadd a b)) (= cfg cfg.next) (= imp_res.next (bvadd a (ite (= #b1 cfg) (bvadd (bvnot b) #b00000001) b))))
PROP
	(= spec_res imp_res)
None
KInduction returned unknown
Traceback (most recent call last):
  File "/home/xxx/pono/examples/python-api/simple_alu.py", line 159, in <module>
    interpolant_attempt()
  File "/home/xxx/pono/examples/python-api/simple_alu.py", line 82, in interpolant_attempt
    s = ss.create_msat_solver(False)
AttributeError: module 'smt_switch' has no attribute 'create_msat_solver'

Process finished with exit code 1

Allow out-of-tree dependencies

Currently, the build scripts assume that dependenices like smt-switch and btor2tools are in the deps folder. We should allow building/installing these separately and specifying their paths.

Implement Lazy Abstraction: Visible variables for FTS

Clean up array axiom enumeration

See comments on #69 for files refiners/axiom_enumerator.h and refiners/array_axiom_enumerator.h for more info.

Return consecutive and nonconsecutive axioms as const references
Pass axiom sets by reference to index_axioms and non_index_axioms
Populate a new vector with axioms after reducing (this should be discussed but I think it's the only way to do it while using references to the axiom sets)

cmake failed by not found gmp

CMake Error at CMakeLists.txt:69 (find_package):
  By not providing "FindGMP.cmake" in CMAKE_MODULE_PATH this project has
  asked CMake to find a package configuration file provided by "GMP", but
  CMake did not find one.

  Could not find a package configuration file provided by "GMP" with any of
  the following names:

    GMPConfig.cmake
    gmp-config.cmake

  Add the installation prefix of "GMP" to CMAKE_PREFIX_PATH or set "GMP_DIR"
  to a directory containing one of the above files.  If "GMP" provides a
  separate development package or SDK, be sure it has been installed.

Actually, I have install libgmp-dev by apt

Using old version of smt-switch

A recent bug fix was made in smt-switch: stanford-centaur/smt-switch#321

The version of smt-switch installed by contrib/setup-smt-switch.sh does not use this most recent version.

Don't declare states/inputs up front

There are often scenarios where an input needs to be "promoted" to a state variable based on some added constraints (important for soundness!). This is much easier to do if they are not declared beforehand, but instead marked as states later.

Rename default branch to main

We should rename the master branch to main. See here for the rationale: https://about.gitlab.com/blog/2021/03/10/new-git-default-branch-name/.

step function of the interpolantion engine is not aligned with other engines

Constraint Handling

Hi I have a question about the part that handles Btor2 constraints.

Suppose that the expression of the constraint is C.
What the code does is: if C does not contain input, then C(V) and C(V') will be added to the transition relation.
But if C contains input, only C(V) will be added to the transition relation.

https://github.com/upscale-project/pono/blob/6d726131aef3179be970570603ab8ca1a38c8f7a/core/ts.cpp#L170

But why is that (I mean why there is such a difference)?

Furthermore, what if C syntactically contains some input variable, but semantically that input variable is reducible (I know that Boolector will do some reduction that may be able to remove it, but I guess there might also be cases where Boolector is not smart enough to do so). Does it matter? Would anything bad happen in this case?

Error during the build of the last commit, Cython related

I'm trying to build an updated version
6d72613 in Docker. And receive some errors from Cython files. Have you seen this before?

[ 55%] Generating CXX source python/pono.cxx

Error compiling Cython file:
------------------------------------------------------------
...
        void add_constraint(const c_Term & constraint) except +
        void name_term(const string name, const c_Term & t) except +
        c_Term make_inputvar(const string name, const c_Sort & sort) except +
        c_Term make_statevar(const string name, const c_Sort & sort) except +
        c_Term curr(const c_Term & term) except +
        c_Term next(const c_Term & ter  m) except +
                                       ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxd:27:40: Expected ')', found 'm'

Error compiling Cython file:
------------------------------------------------------------
...
from libcpp.string cimport string
from libcpp.unordered_set cimport unordered_set
from libcpp.unordered_map cimport unordered_map
from libcpp.vector cimport vector

from pono_imp cimport TransitionSystem as c_TransitionSystem
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:8:0: 'pono_imp/TransitionSystem.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from libcpp.unordered_set cimport unordered_set
from libcpp.unordered_map cimport unordered_map
from libcpp.vector cimport vector

from pono_imp cimport TransitionSystem as c_TransitionSystem
from pono_imp cimport RelationalTransitionSystem as c_RelationalTransitionSystem
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:9:0: 'pono_imp/RelationalTransitionSystem.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from libcpp.unordered_map cimport unordered_map
from libcpp.vector cimport vector

from pono_imp cimport TransitionSystem as c_TransitionSystem
from pono_imp cimport RelationalTransitionSystem as c_RelationalTransitionSystem
from pono_imp cimport FunctionalTransitionSystem as c_FunctionalTransitionSystem
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:10:0: 'pono_imp/FunctionalTransitionSystem.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from libcpp.vector cimport vector

from pono_imp cimport TransitionSystem as c_TransitionSystem
from pono_imp cimport RelationalTransitionSystem as c_RelationalTransitionSystem
from pono_imp cimport FunctionalTransitionSystem as c_FunctionalTransitionSystem
from pono_imp cimport Property as c_Property
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:11:0: 'pono_imp/Property.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...

from pono_imp cimport TransitionSystem as c_TransitionSystem
from pono_imp cimport RelationalTransitionSystem as c_RelationalTransitionSystem
from pono_imp cimport FunctionalTransitionSystem as c_FunctionalTransitionSystem
from pono_imp cimport Property as c_Property
from pono_imp cimport Unroller as c_Unroller
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:12:0: 'pono_imp/Unroller.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport TransitionSystem as c_TransitionSystem
from pono_imp cimport RelationalTransitionSystem as c_RelationalTransitionSystem
from pono_imp cimport FunctionalTransitionSystem as c_FunctionalTransitionSystem
from pono_imp cimport Property as c_Property
from pono_imp cimport Unroller as c_Unroller
from pono_imp cimport ProverResult as c_ProverResult
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:13:0: 'pono_imp/ProverResult.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport RelationalTransitionSystem as c_RelationalTransitionSystem
from pono_imp cimport FunctionalTransitionSystem as c_FunctionalTransitionSystem
from pono_imp cimport Property as c_Property
from pono_imp cimport Unroller as c_Unroller
from pono_imp cimport ProverResult as c_ProverResult
from pono_imp cimport UNKNOWN as c_UNKNOWN
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:14:0: 'pono_imp/UNKNOWN.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport FunctionalTransitionSystem as c_FunctionalTransitionSystem
from pono_imp cimport Property as c_Property
from pono_imp cimport Unroller as c_Unroller
from pono_imp cimport ProverResult as c_ProverResult
from pono_imp cimport UNKNOWN as c_UNKNOWN
from pono_imp cimport FALSE as c_FALSE
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:15:0: 'pono_imp/FALSE.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport Property as c_Property
from pono_imp cimport Unroller as c_Unroller
from pono_imp cimport ProverResult as c_ProverResult
from pono_imp cimport UNKNOWN as c_UNKNOWN
from pono_imp cimport FALSE as c_FALSE
from pono_imp cimport TRUE as c_TRUE
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:16:0: 'pono_imp/TRUE.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport Unroller as c_Unroller
from pono_imp cimport ProverResult as c_ProverResult
from pono_imp cimport UNKNOWN as c_UNKNOWN
from pono_imp cimport FALSE as c_FALSE
from pono_imp cimport TRUE as c_TRUE
from pono_imp cimport Prover as c_Prover
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:17:0: 'pono_imp/Prover.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport ProverResult as c_ProverResult
from pono_imp cimport UNKNOWN as c_UNKNOWN
from pono_imp cimport FALSE as c_FALSE
from pono_imp cimport TRUE as c_TRUE
from pono_imp cimport Prover as c_Prover
from pono_imp cimport Bmc as c_Bmc
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:18:0: 'pono_imp/Bmc.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport UNKNOWN as c_UNKNOWN
from pono_imp cimport FALSE as c_FALSE
from pono_imp cimport TRUE as c_TRUE
from pono_imp cimport Prover as c_Prover
from pono_imp cimport Bmc as c_Bmc
from pono_imp cimport KInduction as c_KInduction
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:19:0: 'pono_imp/KInduction.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport FALSE as c_FALSE
from pono_imp cimport TRUE as c_TRUE
from pono_imp cimport Prover as c_Prover
from pono_imp cimport Bmc as c_Bmc
from pono_imp cimport KInduction as c_KInduction
from pono_imp cimport BmcSimplePath as c_BmcSimplePath
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:20:0: 'pono_imp/BmcSimplePath.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport TRUE as c_TRUE
from pono_imp cimport Prover as c_Prover
from pono_imp cimport Bmc as c_Bmc
from pono_imp cimport KInduction as c_KInduction
from pono_imp cimport BmcSimplePath as c_BmcSimplePath
from pono_imp cimport InterpolantMC as c_InterpolantMC
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:21:0: 'pono_imp/InterpolantMC.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport Prover as c_Prover
from pono_imp cimport Bmc as c_Bmc
from pono_imp cimport KInduction as c_KInduction
from pono_imp cimport BmcSimplePath as c_BmcSimplePath
from pono_imp cimport InterpolantMC as c_InterpolantMC
from pono_imp cimport BTOR2Encoder as c_BTOR2Encoder
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:22:0: 'pono_imp/BTOR2Encoder.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport InterpolantMC as c_InterpolantMC
from pono_imp cimport BTOR2Encoder as c_BTOR2Encoder
IF WITH_COREIR == "ON":
    from pono_imp cimport Module as c_Module
    from pono_imp cimport CoreIREncoder as c_CoreIREncoder
from pono_imp cimport set_global_logger_verbosity as c_set_global_logger_verbosity
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:26:0: 'pono_imp/set_global_logger_verbosity.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport BTOR2Encoder as c_BTOR2Encoder
IF WITH_COREIR == "ON":
    from pono_imp cimport Module as c_Module
    from pono_imp cimport CoreIREncoder as c_CoreIREncoder
from pono_imp cimport set_global_logger_verbosity as c_set_global_logger_verbosity
from pono_imp cimport get_free_symbols as c_get_free_symbols
^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:27:0: 'pono_imp/get_free_symbols.pxd' not found

Error compiling Cython file:
------------------------------------------------------------
...

ctypedef const unordered_map[c_Term, c_Term]* const_UnorderedTermMapPtr
ctypedef unordered_map[c_Term, c_Term].const_iterator c_UnorderedTermMap_const_iterator

cdef class __AbstractTransitionSystem:
    cdef c_TransitionSystem* cts
        ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:51:9: 'c_TransitionSystem' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...
        self.cts = new c_FunctionalTransitionSystem(s.css)
        self._solver = s


cdef class Property:
    cdef c_Property* cp
        ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:310:9: 'c_Property' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...
    def transition_system(self):
        return self.ts


cdef class Unroller:
    cdef c_Unroller* cu
        ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:328:9: 'c_Unroller' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...
        term.ct = dref(self.cu).untime(t.ct)
        return term


cdef class __AbstractProver:
    cdef c_Prover* cp
        ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:346:9: 'c_Prover' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...
        self.cp = new c_InterpolantMC(p.cp[0], s.css, interp.css)
        self._solver = s


cdef class BTOR2Encoder:
    cdef c_BTOR2Encoder * cbe
        ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:430:9: 'c_BTOR2Encoder' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...
    cdef SmtSolver _solver
    # Note: don't want to allow null TransitionSystems
    # means there's no way to instantiate a transition system without the solver
    def __cinit__(self, SmtSolver s):
        # if not specified, this creates a relational transition system under the hood
        self.cts = new c_RelationalTransitionSystem(s.css)
                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:57:23: 'c_RelationalTransitionSystem' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...
    cdef SmtSolver _solver
    # Note: don't want to allow null TransitionSystems
    # means there's no way to instantiate a transition system without the solver
    def __cinit__(self, SmtSolver s):
        # if not specified, this creates a relational transition system under the hood
        self.cts = new c_RelationalTransitionSystem(s.css)
                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:57:23: new operator can only be applied to a C++ class

Error compiling Cython file:
------------------------------------------------------------
...
        # if not specified, this creates a relational transition system under the hood
        self.cts = new c_RelationalTransitionSystem(s.css)
        self._solver = s

    def set_init(self, Term init):
        dref(self.cts).set_init(init.ct)
                                   ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:61:36: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...

    def set_init(self, Term init):
        dref(self.cts).set_init(init.ct)

    def constrain_init(self, Term constraint):
        dref(self.cts).constrain_init(constraint.ct)
                                               ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:64:48: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...

    def constrain_init(self, Term constraint):
        dref(self.cts).constrain_init(constraint.ct)

    def assign_next(self, Term state, Term val):
        dref(self.cts).assign_next(state.ct, val.ct)
                                       ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:67:40: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...

    def constrain_init(self, Term constraint):
        dref(self.cts).constrain_init(constraint.ct)

    def assign_next(self, Term state, Term val):
        dref(self.cts).assign_next(state.ct, val.ct)
                                               ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:67:48: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...

    def assign_next(self, Term state, Term val):
        dref(self.cts).assign_next(state.ct, val.ct)

    def add_invar(self, Term constraint):
        dref(self.cts).add_invar(constraint.ct)
                                          ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:70:43: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...

    def add_invar(self, Term constraint):
        dref(self.cts).add_invar(constraint.ct)

    def constrain_inputs(self, Term constraint):
        dref(self.cts).constrain_inputs(constraint.ct)
                                                 ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:73:50: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...

    def constrain_inputs(self, Term constraint):
        dref(self.cts).constrain_inputs(constraint.ct)

    def add_constraint(self, Term constraint):
        dref(self.cts).add_constraint(constraint.ct)
                                               ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:76:48: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...

    def add_constraint(self, Term constraint):
        dref(self.cts).add_constraint(constraint.ct)

    def name_term(self, str name, Term t):
        dref(self.cts).name_term(name.encode(), t.ct)
                                                ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:79:49: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
    def name_term(self, str name, Term t):
        dref(self.cts).name_term(name.encode(), t.ct)

    def make_inputvar(self, str name, Sort sort):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cts).make_inputvar(name.encode(), sort.cs)
                                                                 ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:83:66: Cannot convert 'c_Sort' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
    def name_term(self, str name, Term t):
        dref(self.cts).name_term(name.encode(), t.ct)

    def make_inputvar(self, str name, Sort sort):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cts).make_inputvar(name.encode(), sort.cs)
                                             ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:83:46: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...
        term.ct = dref(self.cts).make_inputvar(name.encode(), sort.cs)
        return term

    def make_statevar(self, str name, Sort sort):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cts).make_statevar(name.encode(), sort.cs)
                                                                 ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:88:66: Cannot convert 'c_Sort' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
        term.ct = dref(self.cts).make_inputvar(name.encode(), sort.cs)
        return term

    def make_statevar(self, str name, Sort sort):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cts).make_statevar(name.encode(), sort.cs)
                                             ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:88:46: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...
        term.ct = dref(self.cts).make_statevar(name.encode(), sort.cs)
        return term

    def curr(self, Term t):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cts).curr(t.ct)
                                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:93:39: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
        term.ct = dref(self.cts).make_statevar(name.encode(), sort.cs)
        return term

    def curr(self, Term t):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cts).curr(t.ct)
                                    ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:93:37: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...
        term.ct = dref(self.cts).curr(t.ct)
        return term

    def next(self, Term t):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cts).next(t.ct)
                                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:98:39: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
        term.ct = dref(self.cts).curr(t.ct)
        return term

    def next(self, Term t):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cts).next(t.ct)
                                    ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:98:37: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cts).next(t.ct)
        return term

    def is_curr_var(self, Term sv):
        return dref(self.cts).is_curr_var(sv.ct)
                                           ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:102:44: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...

    def is_curr_var(self, Term sv):
        return dref(self.cts).is_curr_var(sv.ct)

    def is_next_var(self, Term sv):
        return dref(self.cts).is_next_var(sv.ct)
                                           ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:105:44: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...

    @property
    def statevars(self):
        states_set = set()

        cdef const_UnorderedTermSetPtr c_states_set = &dref(self.cts).statevars()
                                                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:115:54: Taking address of non-lvalue (type Python object)

Error compiling Cython file:
------------------------------------------------------------
...

    @property
    def inputvars(self):
        inputs_set = set()

        cdef const_UnorderedTermSetPtr c_inputs_set = &dref(self.cts).inputvars()
                                                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:132:54: Taking address of non-lvalue (type Python object)

Error compiling Cython file:
------------------------------------------------------------
...

    @property
    def state_updates(self):
        updates = {}

        cdef const_UnorderedTermMapPtr c_updates_map = &dref(self.cts).state_updates()
                                                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:149:55: Taking address of non-lvalue (type Python object)

Error compiling Cython file:
------------------------------------------------------------
...

    @property
    def named_terms(self):
        names2terms = {}

        cdef unordered_map[string, c_Term]* c_named_terms = &dref(self.cts).named_terms()
                                                           ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:169:60: Taking address of non-lvalue (type Python object)

Error compiling Cython file:
------------------------------------------------------------
...
        return names2terms

    @property
    def constraints(self):
        convec = []
        cdef c_TermVec c_cons = dref(self.cts).constraints()
                                                         ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:185:58: Cannot convert Python object to 'c_TermVec'

Error compiling Cython file:
------------------------------------------------------------
...
        return convec

    @property
    def init(self):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cts).init()
                                    ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:195:37: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...
        return term

    @property
    def trans(self):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cts).trans()
                                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:201:38: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...
        cdef Sort s = Sort(self)
        cdef c_SortKind sk
        cdef c_SortVec csv

        if isinstance(arg0, str):
            s.cs = dref(self.cts).make_sort(<const string> arg0.encode(), <int?> arg1)
                                          ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:213:43: Cannot convert Python object to 'c_Sort'

Error compiling Cython file:
------------------------------------------------------------
...
        if isinstance(arg0, str):
            s.cs = dref(self.cts).make_sort(<const string> arg0.encode(), <int?> arg1)
        elif isinstance(arg0, SortKind):
            sk = (<SortKind> arg0).sk
            if arg1 is None:
                s.cs = dref(self.cts).make_sort(sk)
                                               ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:217:48: Cannot convert 'c_SortKind' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
        if isinstance(arg0, str):
            s.cs = dref(self.cts).make_sort(<const string> arg0.encode(), <int?> arg1)
        elif isinstance(arg0, SortKind):
            sk = (<SortKind> arg0).sk
            if arg1 is None:
                s.cs = dref(self.cts).make_sort(sk)
                                              ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:217:47: Cannot convert Python object to 'c_Sort'

Error compiling Cython file:
------------------------------------------------------------
...
        elif isinstance(arg0, SortKind):
            sk = (<SortKind> arg0).sk
            if arg1 is None:
                s.cs = dref(self.cts).make_sort(sk)
            elif isinstance(arg1, int) and arg2 is None:
                s.cs = dref(self.cts).make_sort(sk, <int> arg1)
                                               ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:219:48: Cannot convert 'c_SortKind' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
        elif isinstance(arg0, SortKind):
            sk = (<SortKind> arg0).sk
            if arg1 is None:
                s.cs = dref(self.cts).make_sort(sk)
            elif isinstance(arg1, int) and arg2 is None:
                s.cs = dref(self.cts).make_sort(sk, <int> arg1)
                                              ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:219:47: Cannot convert Python object to 'c_Sort'

Error compiling Cython file:
------------------------------------------------------------
...
            if arg1 is None:
                s.cs = dref(self.cts).make_sort(sk)
            elif isinstance(arg1, int) and arg2 is None:
                s.cs = dref(self.cts).make_sort(sk, <int> arg1)
            elif isinstance(arg1, Sort) and arg2 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort> arg1).cs)
                                               ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:221:48: Cannot convert 'c_SortKind' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
            if arg1 is None:
                s.cs = dref(self.cts).make_sort(sk)
            elif isinstance(arg1, int) and arg2 is None:
                s.cs = dref(self.cts).make_sort(sk, <int> arg1)
            elif isinstance(arg1, Sort) and arg2 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort> arg1).cs)
                                                                ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:221:65: Cannot convert 'c_Sort' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
            if arg1 is None:
                s.cs = dref(self.cts).make_sort(sk)
            elif isinstance(arg1, int) and arg2 is None:
                s.cs = dref(self.cts).make_sort(sk, <int> arg1)
            elif isinstance(arg1, Sort) and arg2 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort> arg1).cs)
                                              ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:221:47: Cannot convert Python object to 'c_Sort'

Error compiling Cython file:
------------------------------------------------------------
...
            elif isinstance(arg1, Sort) and arg2 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort> arg1).cs)
            elif isinstance(arg1, list) and arg2 is None:
                for a in arg1:
                    csv.push_back((<Sort?> a).cs)
                s.cs = dref(self.cts).make_sort(sk, csv)
                                               ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:225:48: Cannot convert 'c_SortKind' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
            elif isinstance(arg1, Sort) and arg2 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort> arg1).cs)
            elif isinstance(arg1, list) and arg2 is None:
                for a in arg1:
                    csv.push_back((<Sort?> a).cs)
                s.cs = dref(self.cts).make_sort(sk, csv)
                                                   ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:225:52: Cannot convert 'c_SortVec' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
            elif isinstance(arg1, Sort) and arg2 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort> arg1).cs)
            elif isinstance(arg1, list) and arg2 is None:
                for a in arg1:
                    csv.push_back((<Sort?> a).cs)
                s.cs = dref(self.cts).make_sort(sk, csv)
                                              ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:225:47: Cannot convert Python object to 'c_Sort'

Error compiling Cython file:
------------------------------------------------------------
...
            elif isinstance(arg1, list) and arg2 is None:
                for a in arg1:
                    csv.push_back((<Sort?> a).cs)
                s.cs = dref(self.cts).make_sort(sk, csv)
            elif arg3 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
                                               ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:227:48: Cannot convert 'c_SortKind' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
            elif isinstance(arg1, list) and arg2 is None:
                for a in arg1:
                    csv.push_back((<Sort?> a).cs)
                s.cs = dref(self.cts).make_sort(sk, csv)
            elif arg3 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
                                                                 ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:227:66: Cannot convert 'c_Sort' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
            elif isinstance(arg1, list) and arg2 is None:
                for a in arg1:
                    csv.push_back((<Sort?> a).cs)
                s.cs = dref(self.cts).make_sort(sk, csv)
            elif arg3 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
                                                                                    ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:227:85: Cannot convert 'c_Sort' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
            elif isinstance(arg1, list) and arg2 is None:
                for a in arg1:
                    csv.push_back((<Sort?> a).cs)
                s.cs = dref(self.cts).make_sort(sk, csv)
            elif arg3 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
                                              ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:227:47: Cannot convert Python object to 'c_Sort'

Error compiling Cython file:
------------------------------------------------------------
...
                    csv.push_back((<Sort?> a).cs)
                s.cs = dref(self.cts).make_sort(sk, csv)
            elif arg3 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
            elif arg3 is not None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs,
                                               ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:229:48: Cannot convert 'c_SortKind' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
                    csv.push_back((<Sort?> a).cs)
                s.cs = dref(self.cts).make_sort(sk, csv)
            elif arg3 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
            elif arg3 is not None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs,
                                                                 ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:229:66: Cannot convert 'c_Sort' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
                s.cs = dref(self.cts).make_sort(sk, csv)
            elif arg3 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
            elif arg3 is not None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs,
                                                    (<Sort?> arg2).cs,
                                                                 ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:230:66: Cannot convert 'c_Sort' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
            elif arg3 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
            elif arg3 is not None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs,
                                                    (<Sort?> arg2).cs,
                                                    (<Sort?> arg3).cs)
                                                                 ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:231:66: Cannot convert 'c_Sort' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
                    csv.push_back((<Sort?> a).cs)
                s.cs = dref(self.cts).make_sort(sk, csv)
            elif arg3 is None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
            elif arg3 is not None:
                s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs,
                                              ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:229:47: Cannot convert Python object to 'c_Sort'

Error compiling Cython file:
------------------------------------------------------------
...
            if not args:
                raise ValueError("Can't call make_term with an Op ({}) and no arguments".format(op_or_val))

            for a in args:
                ctv.push_back((<Term?> a).ct)
            term.ct = dref(self.cts).make_term((<Op> op_or_val).op, ctv)
                                                              ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:267:63: Cannot convert 'c_Op' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
            if not args:
                raise ValueError("Can't call make_term with an Op ({}) and no arguments".format(op_or_val))

            for a in args:
                ctv.push_back((<Term?> a).ct)
            term.ct = dref(self.cts).make_term((<Op> op_or_val).op, ctv)
                                                                   ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:267:68: Cannot convert 'c_TermVec' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
            if not args:
                raise ValueError("Can't call make_term with an Op ({}) and no arguments".format(op_or_val))

            for a in args:
                ctv.push_back((<Term?> a).ct)
            term.ct = dref(self.cts).make_term((<Op> op_or_val).op, ctv)
                                             ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:267:46: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...

            for a in args:
                ctv.push_back((<Term?> a).ct)
            term.ct = dref(self.cts).make_term((<Op> op_or_val).op, ctv)
        elif isinstance(op_or_val, bool) and len(args) == 0:
            term.ct = dref(self.cts).make_term(<bint> op_or_val)
                                             ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:269:46: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...
                ctv.push_back((<Term?> a).ct)
            term.ct = dref(self.cts).make_term((<Op> op_or_val).op, ctv)
        elif isinstance(op_or_val, bool) and len(args) == 0:
            term.ct = dref(self.cts).make_term(<bint> op_or_val)
        elif isinstance(op_or_val, str) and len(args) == 1 and isinstance(args[0], Sort):
            term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(), (<Sort> args[0]).cs)
                                                                                                 ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:271:98: Cannot convert 'c_Sort' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
                ctv.push_back((<Term?> a).ct)
            term.ct = dref(self.cts).make_term((<Op> op_or_val).op, ctv)
        elif isinstance(op_or_val, bool) and len(args) == 0:
            term.ct = dref(self.cts).make_term(<bint> op_or_val)
        elif isinstance(op_or_val, str) and len(args) == 1 and isinstance(args[0], Sort):
            term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(), (<Sort> args[0]).cs)
                                             ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:271:46: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...
            term.ct = dref(self.cts).make_term(<bint> op_or_val)
        elif isinstance(op_or_val, str) and len(args) == 1 and isinstance(args[0], Sort):
            term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(), (<Sort> args[0]).cs)
        elif isinstance(op_or_val, str) and len(args) == 2 and isinstance(args[0], Sort):
            term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(),
                                               (<Sort> args[0]).cs,
                                                              ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:274:63: Cannot convert 'c_Sort' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
        elif isinstance(op_or_val, bool) and len(args) == 0:
            term.ct = dref(self.cts).make_term(<bint> op_or_val)
        elif isinstance(op_or_val, str) and len(args) == 1 and isinstance(args[0], Sort):
            term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(), (<Sort> args[0]).cs)
        elif isinstance(op_or_val, str) and len(args) == 2 and isinstance(args[0], Sort):
            term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(),
                                             ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:273:46: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...
            term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(),
                                               (<Sort> args[0]).cs,
                                               <int?> args[1])
        elif isinstance(op_or_val, int) and len(args) == 1 and isinstance(args[0], Sort):
            # always use the string representation of integers (to handle large ints)
            term.ct = dref(self.cts).make_term((<const string?> str(op_or_val).encode()), (<Sort> args[0]).cs)
                                                                                                         ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:278:106: Cannot convert 'c_Sort' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
            term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(),
                                               (<Sort> args[0]).cs,
                                               <int?> args[1])
        elif isinstance(op_or_val, int) and len(args) == 1 and isinstance(args[0], Sort):
            # always use the string representation of integers (to handle large ints)
            term.ct = dref(self.cts).make_term((<const string?> str(op_or_val).encode()), (<Sort> args[0]).cs)
                                             ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:278:46: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...
        elif isinstance(op_or_val, int) and len(args) == 1 and isinstance(args[0], Sort):
            # always use the string representation of integers (to handle large ints)
            term.ct = dref(self.cts).make_term((<const string?> str(op_or_val).encode()), (<Sort> args[0]).cs)
        elif isinstance(op_or_val, Term) and len(args) == 1 and isinstance(args[0], Sort):
            # this is for creating a constant array
            term.ct = dref(self.cts).make_term((<Term?> op_or_val).ct, (<Sort?> args[0]).cs)
                                                                 ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:281:66: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
        elif isinstance(op_or_val, int) and len(args) == 1 and isinstance(args[0], Sort):
            # always use the string representation of integers (to handle large ints)
            term.ct = dref(self.cts).make_term((<const string?> str(op_or_val).encode()), (<Sort> args[0]).cs)
        elif isinstance(op_or_val, Term) and len(args) == 1 and isinstance(args[0], Sort):
            # this is for creating a constant array
            term.ct = dref(self.cts).make_term((<Term?> op_or_val).ct, (<Sort?> args[0]).cs)
                                                                                       ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:281:88: Cannot convert 'c_Sort' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
        elif isinstance(op_or_val, int) and len(args) == 1 and isinstance(args[0], Sort):
            # always use the string representation of integers (to handle large ints)
            term.ct = dref(self.cts).make_term((<const string?> str(op_or_val).encode()), (<Sort> args[0]).cs)
        elif isinstance(op_or_val, Term) and len(args) == 1 and isinstance(args[0], Sort):
            # this is for creating a constant array
            term.ct = dref(self.cts).make_term((<Term?> op_or_val).ct, (<Sort?> args[0]).cs)
                                             ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:281:46: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...
        return term


cdef class RelationalTransitionSystem(__AbstractTransitionSystem):
    def __cinit__(self, SmtSolver s):
        self.cts = new c_RelationalTransitionSystem(s.css)
                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:290:23: 'c_RelationalTransitionSystem' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...
        return term


cdef class RelationalTransitionSystem(__AbstractTransitionSystem):
    def __cinit__(self, SmtSolver s):
        self.cts = new c_RelationalTransitionSystem(s.css)
                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:290:23: new operator can only be applied to a C++ class

Error compiling Cython file:
------------------------------------------------------------
...
    def __cinit__(self, SmtSolver s):
        self.cts = new c_RelationalTransitionSystem(s.css)
        self._solver = s

    def set_behavior(self, Term init, Term trans):
        dref(<c_RelationalTransitionSystem * ?> self.cts).set_behavior(init.ct, trans.ct)
             ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:294:14: 'c_RelationalTransitionSystem' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...
    def __cinit__(self, SmtSolver s):
        self.cts = new c_RelationalTransitionSystem(s.css)
        self._solver = s

    def set_behavior(self, Term init, Term trans):
        dref(<c_RelationalTransitionSystem * ?> self.cts).set_behavior(init.ct, trans.ct)
                                                                          ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:294:75: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
    def __cinit__(self, SmtSolver s):
        self.cts = new c_RelationalTransitionSystem(s.css)
        self._solver = s

    def set_behavior(self, Term init, Term trans):
        dref(<c_RelationalTransitionSystem * ?> self.cts).set_behavior(init.ct, trans.ct)
                                                                                    ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:294:85: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...

    def set_behavior(self, Term init, Term trans):
        dref(<c_RelationalTransitionSystem * ?> self.cts).set_behavior(init.ct, trans.ct)

    def set_trans(self, Term trans):
        dref(<c_RelationalTransitionSystem * ?> self.cts).set_trans(trans.ct)
             ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:297:14: 'c_RelationalTransitionSystem' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...

    def set_behavior(self, Term init, Term trans):
        dref(<c_RelationalTransitionSystem * ?> self.cts).set_behavior(init.ct, trans.ct)

    def set_trans(self, Term trans):
        dref(<c_RelationalTransitionSystem * ?> self.cts).set_trans(trans.ct)
                                                                        ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:297:73: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...

    def set_trans(self, Term trans):
        dref(<c_RelationalTransitionSystem * ?> self.cts).set_trans(trans.ct)

    def constrain_trans(self, Term constraint):
        dref(<c_RelationalTransitionSystem * ?> self.cts).constrain_trans(constraint.ct)
             ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:300:14: 'c_RelationalTransitionSystem' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...

    def set_trans(self, Term trans):
        dref(<c_RelationalTransitionSystem * ?> self.cts).set_trans(trans.ct)

    def constrain_trans(self, Term constraint):
        dref(<c_RelationalTransitionSystem * ?> self.cts).constrain_trans(constraint.ct)
                                                                                   ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:300:84: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
        dref(<c_RelationalTransitionSystem * ?> self.cts).constrain_trans(constraint.ct)


cdef class FunctionalTransitionSystem(__AbstractTransitionSystem):
    def __cinit__(self, SmtSolver s):
        self.cts = new c_FunctionalTransitionSystem(s.css)
                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:305:23: 'c_FunctionalTransitionSystem' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...
        dref(<c_RelationalTransitionSystem * ?> self.cts).constrain_trans(constraint.ct)


cdef class FunctionalTransitionSystem(__AbstractTransitionSystem):
    def __cinit__(self, SmtSolver s):
        self.cts = new c_FunctionalTransitionSystem(s.css)
                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:305:23: new operator can only be applied to a C++ class

Error compiling Cython file:
------------------------------------------------------------
...

cdef class Property:
    cdef c_Property* cp
    cdef __AbstractTransitionSystem ts
    def __cinit__(self, __AbstractTransitionSystem ts, Term p):
        self.cp = new c_Property(ts.cts[0], p.ct)
                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:313:22: 'c_Property' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...

cdef class Property:
    cdef c_Property* cp
    cdef __AbstractTransitionSystem ts
    def __cinit__(self, __AbstractTransitionSystem ts, Term p):
        self.cp = new c_Property(ts.cts[0], p.ct)
                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:313:22: new operator can only be applied to a C++ class

Error compiling Cython file:
------------------------------------------------------------
...
        self.ts = ts

    @property
    def prop(self):
        cdef Term p = Term(self.ts.solver)
        p.ct = dref(self.cp).prop()
                                ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:319:33: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...

cdef class Unroller:
    cdef c_Unroller* cu
    cdef SmtSolver _solver
    def __cinit__(self, __AbstractTransitionSystem ts, SmtSolver s):
        self.cu = new c_Unroller(ts.cts[0], s.css)
                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:331:22: 'c_Unroller' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...

cdef class Unroller:
    cdef c_Unroller* cu
    cdef SmtSolver _solver
    def __cinit__(self, __AbstractTransitionSystem ts, SmtSolver s):
        self.cu = new c_Unroller(ts.cts[0], s.css)
                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:331:22: new operator can only be applied to a C++ class

Error compiling Cython file:
------------------------------------------------------------
...
        self.cu = new c_Unroller(ts.cts[0], s.css)
        self._solver = s

    def at_time(self, Term t, unsigned int k):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cu).at_time(t.ct, k)
                                        ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:336:41: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
        self.cu = new c_Unroller(ts.cts[0], s.css)
        self._solver = s

    def at_time(self, Term t, unsigned int k):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cu).at_time(t.ct, k)
                                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:336:39: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...
        term.ct = dref(self.cu).at_time(t.ct, k)
        return term

    def untime(self, Term t):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cu).untime(t.ct)
                                       ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:341:40: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
        term.ct = dref(self.cu).at_time(t.ct, k)
        return term

    def untime(self, Term t):
        cdef Term term = Term(self._solver)
        term.ct = dref(self.cu).untime(t.ct)
                                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:341:38: Cannot convert Python object to 'c_Term'

Error compiling Cython file:
------------------------------------------------------------
...
    def check_until(self, int k):
        '''
        Checks until bound k, returns True, False or None (if unknown)
        '''
        cdef int r = <int> dref(self.cp).check_until(k)
        if r == (<int> c_UNKNOWN):
                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:358:23: 'c_UNKNOWN' is not a constant, variable or function identifier

Error compiling Cython file:
------------------------------------------------------------
...
        Checks until bound k, returns True, False or None (if unknown)
        '''
        cdef int r = <int> dref(self.cp).check_until(k)
        if r == (<int> c_UNKNOWN):
            return None
        elif r == (<int> c_FALSE):
                        ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:360:25: 'c_FALSE' is not a constant, variable or function identifier

Error compiling Cython file:
------------------------------------------------------------
...
        cdef int r = <int> dref(self.cp).check_until(k)
        if r == (<int> c_UNKNOWN):
            return None
        elif r == (<int> c_FALSE):
            return False
        elif r == (<int> c_TRUE):
                        ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:362:25: 'c_TRUE' is not a constant, variable or function identifier

Error compiling Cython file:
------------------------------------------------------------
...
        elif r == (<int> c_TRUE):
            return True

    def witness(self):
        cdef vector[c_UnorderedTermMap] cw
        success = dref(self.cp).witness(cw)
                                       ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:367:40: Cannot convert 'vector[c_UnorderedTermMap]' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
        '''
        Tries to prove property unboundedly, returns True, False or None (if unknown)
        '''
        cdef int r = <int> dref(self.cp).prove()

        if r == (<int> c_UNKNOWN):
                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:393:23: 'c_UNKNOWN' is not a constant, variable or function identifier

Error compiling Cython file:
------------------------------------------------------------
...
        '''
        cdef int r = <int> dref(self.cp).prove()

        if r == (<int> c_UNKNOWN):
            return None
        elif r == (<int> c_FALSE):
                        ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:395:25: 'c_FALSE' is not a constant, variable or function identifier

Error compiling Cython file:
------------------------------------------------------------
...

        if r == (<int> c_UNKNOWN):
            return None
        elif r == (<int> c_FALSE):
            return False
        elif r == (<int> c_TRUE):
                        ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:397:25: 'c_TRUE' is not a constant, variable or function identifier

Error compiling Cython file:
------------------------------------------------------------
...
        return self._property


cdef class Bmc(__AbstractProver):
    def __cinit__(self, Property p, SmtSolver s):
        self.cp = new c_Bmc(p.cp[0], s.css)
                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:407:22: 'c_Bmc' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...
        return self._property


cdef class Bmc(__AbstractProver):
    def __cinit__(self, Property p, SmtSolver s):
        self.cp = new c_Bmc(p.cp[0], s.css)
                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:407:22: new operator can only be applied to a C++ class

Error compiling Cython file:
------------------------------------------------------------
...
        self._solver = s


cdef class KInduction(__AbstractProver):
    def __cinit__(self, Property p, SmtSolver s):
        self.cp = new c_KInduction(p.cp[0], s.css)
                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:413:22: 'c_KInduction' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...
        self._solver = s


cdef class KInduction(__AbstractProver):
    def __cinit__(self, Property p, SmtSolver s):
        self.cp = new c_KInduction(p.cp[0], s.css)
                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:413:22: new operator can only be applied to a C++ class

Error compiling Cython file:
------------------------------------------------------------
...
        self._solver = s


cdef class BmcSimplePath(__AbstractProver):
    def __cinit__(self, Property p, SmtSolver s):
        self.cp = new c_BmcSimplePath(p.cp[0], s.css)
                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:419:22: 'c_BmcSimplePath' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...
        self._solver = s


cdef class BmcSimplePath(__AbstractProver):
    def __cinit__(self, Property p, SmtSolver s):
        self.cp = new c_BmcSimplePath(p.cp[0], s.css)
                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:419:22: new operator can only be applied to a C++ class

Error compiling Cython file:
------------------------------------------------------------
...
        self._solver = s


cdef class InterpolantMC(__AbstractProver):
    def __cinit__(self, Property p, SmtSolver s, SmtSolver interp):
        self.cp = new c_InterpolantMC(p.cp[0], s.css, interp.css)
                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:425:22: 'c_InterpolantMC' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...
        self._solver = s


cdef class InterpolantMC(__AbstractProver):
    def __cinit__(self, Property p, SmtSolver s, SmtSolver interp):
        self.cp = new c_InterpolantMC(p.cp[0], s.css, interp.css)
                     ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:425:22: new operator can only be applied to a C++ class

Error compiling Cython file:
------------------------------------------------------------
...


cdef class BTOR2Encoder:
    cdef c_BTOR2Encoder * cbe
    def __cinit__(self, str filename, __AbstractTransitionSystem ts):
        self.cbe = new c_BTOR2Encoder(filename.encode(), dref(ts.cts))
                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:432:23: 'c_BTOR2Encoder' is not a type identifier

Error compiling Cython file:
------------------------------------------------------------
...


cdef class BTOR2Encoder:
    cdef c_BTOR2Encoder * cbe
    def __cinit__(self, str filename, __AbstractTransitionSystem ts):
        self.cbe = new c_BTOR2Encoder(filename.encode(), dref(ts.cts))
                      ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:432:23: new operator can only be applied to a C++ class

Error compiling Cython file:
------------------------------------------------------------
...
                raise ValueError("CoreIR encoder takes a pycoreir Context or a filename but got {}".format(mod))



def set_global_logger_verbosity(int v):
    c_set_global_logger_verbosity(v)
   ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:450:4: 'c_set_global_logger_verbosity' is not a constant, variable or function identifier

Error compiling Cython file:
------------------------------------------------------------
...
    c_set_global_logger_verbosity(v)


def get_free_symbols(Term term):
    cdef c_UnorderedTermSet out_symbols
    c_get_free_symbols(term.ct, out_symbols)
   ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:455:4: 'c_get_free_symbols' is not a constant, variable or function identifier

Error compiling Cython file:
------------------------------------------------------------
...
    c_set_global_logger_verbosity(v)


def get_free_symbols(Term term):
    cdef c_UnorderedTermSet out_symbols
    c_get_free_symbols(term.ct, out_symbols)
                          ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:455:27: Cannot convert 'c_Term' to Python object

Error compiling Cython file:
------------------------------------------------------------
...
    c_set_global_logger_verbosity(v)


def get_free_symbols(Term term):
    cdef c_UnorderedTermSet out_symbols
    c_get_free_symbols(term.ct, out_symbols)
                               ^
------------------------------------------------------------

/home/xxx/pono/python/pono_imp.pxi:455:32: Cannot convert 'c_UnorderedTermSet' to Python object
make[2]: *** [python/CMakeFiles/pono.dir/build.make:94: python/pono.cxx] Error 1
make[2]: *** Deleting file 'python/pono.cxx'
make[1]: *** [CMakeFiles/Makefile2:294: python/CMakeFiles/pono.dir/all] Error 2
make: *** [Makefile:160: all] Error 2

Python bindings should use `-undefined dynamic_lookup` when `Py_ENABLE_SHARED` is 0

Walked through the README steps and ran into a seg fault trying to run the test suite:

~/repos/pono master*
base ❯ pytest ./tests
===================================================================== test session starts ======================================================================
platform darwin -- Python 3.8.3, pytest-6.0.0, py-1.9.0, pluggy-0.13.1
rootdir: /Users/lenny/repos/pono
plugins: pycodestyle-2.2.0
collecting ... Fatal Python error: Segmentation fault

Current thread 0x000000011de01dc0 (most recent call first):
  File "<frozen importlib._bootstrap>", line 219 in _call_with_frames_removed
  File "<frozen importlib._bootstrap_external>", line 1101 in create_module
  File "<frozen importlib._bootstrap>", line 556 in module_from_spec
  File "<frozen importlib._bootstrap>", line 657 in _load_unlocked
  File "<frozen importlib._bootstrap>", line 975 in _find_and_load_unlocked
  File "<frozen importlib._bootstrap>", line 991 in _find_and_load
  File "/Users/lenny/repos/pono/tests/python/test_encoders.py", line 2 in <module>
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/assertion/rewrite.py", line 170 in exec_module
  File "<frozen importlib._bootstrap>", line 671 in _load_unlocked
  File "<frozen importlib._bootstrap>", line 975 in _find_and_load_unlocked
  File "<frozen importlib._bootstrap>", line 991 in _find_and_load
  File "<frozen importlib._bootstrap>", line 1014 in _gcd_import
  File "/Users/lenny/miniconda3/lib/python3.8/importlib/__init__.py", line 127 in import_module
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/pathlib.py", line 520 in import_path
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/python.py", line 552 in _importtestmodule
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/python.py", line 484 in _getobj
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/python.py", line 288 in obj
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/python.py", line 500 in _inject_setup_module_fixture
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/python.py", line 487 in collect
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/runner.py", line 324 in <lambda>
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/runner.py", line 294 in from_call
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/runner.py", line 324 in pytest_make_collect_report
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/callers.py", line 187 in _multicall
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/manager.py", line 84 in <lambda>
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/manager.py", line 93 in _hookexec
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/hooks.py", line 286 in __call__
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/runner.py", line 441 in collect_one_node
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 768 in genitems
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 568 in _perform_collect
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 516 in perform_collect
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 306 in pytest_collection
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/callers.py", line 187 in _multicall
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/manager.py", line 84 in <lambda>
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/manager.py", line 93 in _hookexec
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/hooks.py", line 286 in __call__
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 295 in _main
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 240 in wrap_session
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 289 in pytest_cmdline_main
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/callers.py", line 187 in _multicall
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/manager.py", line 84 in <lambda>
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/manager.py", line 93 in _hookexec
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/hooks.py", line 286 in __call__
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/config/__init__.py", line 157 in main
  File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/config/__init__.py", line 180 in console_main
  File "/Users/lenny/miniconda3/bin/pytest", line 8 in <module>
zsh: segmentation fault  pytest ./tests

I traced the issue to the import pono step, here's a backtrace produced by lldb:

~/repos/pono master*
base ❯ lldb -- ~/miniconda3/bin/python -c "import pono"
(lldb) target create "/Users/lenny/miniconda3/bin/python"
Current executable set to '/Users/lenny/miniconda3/bin/python' (x86_64).
(lldb) settings set -- target.run-args  "-c" "import pono"
(lldb) r
Process 98745 launched: '/Users/lenny/miniconda3/bin/python' (x86_64)
Process 98745 stopped
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x8)
    frame #0: 0x0000000104613797 libpython3.8.dylib`PyType_Ready + 455
libpython3.8.dylib`PyType_Ready:
->  0x104613797 <+455>: movq   0x8(%rcx), %rdx
    0x10461379b <+459>: movq   %rax, (%rdx)
    0x10461379e <+462>: movq   -0x8(%rbx), %rsi
    0x1046137a2 <+466>: andl   $0x3, %esi
Target 0: (python) stopped.
(lldb) bt
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x8)
  * frame #0: 0x0000000104613797 libpython3.8.dylib`PyType_Ready + 455
    frame #1: 0x000000010461368f libpython3.8.dylib`PyType_Ready + 191
    frame #2: 0x00000001045f6e99 libpython3.8.dylib`PyModuleDef_Init + 25
    frame #3: 0x00000001001a7645 python`_PyImport_LoadDynamicModuleWithSpec + 565
    frame #4: 0x00000001001a64e5 python`_imp_create_dynamic + 181
    frame #5: 0x000000010008aea4 python`cfunction_vectorcall_FASTCALL + 84
    frame #6: 0x000000010002dbd9 python`PyVectorcall_Call + 121
    frame #7: 0x0000000100164d6f python`_PyEval_EvalFrameDefault + 47711
    frame #8: 0x000000010015752d python`_PyEval_EvalCodeWithName + 557
    frame #9: 0x000000010002e8ca python`_PyFunction_Vectorcall + 426
    frame #10: 0x000000010016430b python`_PyEval_EvalFrameDefault + 45051
    frame #11: 0x000000010002e818 python`_PyFunction_Vectorcall + 248
    frame #12: 0x0000000100164216 python`_PyEval_EvalFrameDefault + 44806
    frame #13: 0x000000010002e818 python`_PyFunction_Vectorcall + 248
    frame #14: 0x000000010016469b python`_PyEval_EvalFrameDefault + 45963
    frame #15: 0x000000010002e818 python`_PyFunction_Vectorcall + 248
    frame #16: 0x000000010016469b python`_PyEval_EvalFrameDefault + 45963
    frame #17: 0x000000010002e818 python`_PyFunction_Vectorcall + 248
    frame #18: 0x000000010016469b python`_PyEval_EvalFrameDefault + 45963
    frame #19: 0x000000010002e818 python`_PyFunction_Vectorcall + 248
    frame #20: 0x0000000100030686 python`object_vacall + 374
    frame #21: 0x000000010003090d python`_PyObject_CallMethodIdObjArgs + 237
    frame #22: 0x00000001001a060e python`PyImport_ImportModuleLevelObject + 1342
    frame #23: 0x00000001001618df python`_PyEval_EvalFrameDefault + 34255
    frame #24: 0x000000010015752d python`_PyEval_EvalCodeWithName + 557
    frame #25: 0x00000001001d2a03 python`PyRun_StringFlags + 259
    frame #26: 0x00000001001d2852 python`PyRun_SimpleStringFlags + 82
    frame #27: 0x00000001001f7ba6 python`pymain_run_command + 134
    frame #28: 0x00000001001f6bdd python`pymain_run_python + 477
    frame #29: 0x00000001001f69a5 python`Py_RunMain + 37
    frame #30: 0x00000001001f7f41 python`pymain_main + 49
    frame #31: 0x0000000100000d68 python`main + 56
    frame #32: 0x00007fff67ed7cc9 libdyld.dylib`start + 1
(lldb)

Have you seen anything like this before? I'm going to try rebuilding from scratch to make sure I didn't mess up a step.

Suggestion to the Yosys Script

Hi,

I was thinking maybe it is helpful to mention the sim command
in the example yosys script, because sometimes, people may need to
use that to drive the reset pin to get the reset state for formal analysis.

I usually use it in the following way:
sim -clock %clockpin% -reset %resetpin% -n 1 -w %top_module%

There are also other useful options (like nreset, zinit, rstlen) from the Yosys's help message

Thanks
Hongce

MSAT related code in create_reducer_for is not guarded by macro

Hi I'm having compilation issues when not using MSAT. Therefore, I'm wondering: maybe this part of code needs to be guarded by macro WITH_MSAT? Thanks!

https://github.com/upscale-project/pono/blob/00c3017e19e373582dce96bddb34a60fa6ec84f4/smt/available_solvers.cpp#L158

Unexpected sort for `neq` operation on arrays

I was testing the following BTOR2 model, which is doing an equality check on two uninitialized arrays:

1 sort bitvec 1
2 sort bitvec 2
3 sort bitvec 8
4 sort array 2 3
5 state 4 mem1
6 state 4 mem2
7 neq 1 5 6
8 bad 7

And for this model pono returns:

Unexpected sort
unknown
b0

Instead of the expected witness with an arbitrary element in the array differing.

Curiously enough, if I only change neq to eq in the model, that works normally:

sat
b0
#0
0 [11] 11111111 mem1@0
0 00000000 mem1@0
1 [11] 11111111 mem2@0
1 00000000 mem2@0
@0
.

Improve interface with original TS

Handling multiple solvers is still ugly. In particular, one area this shows up is when the original transition system is different than the solver used in the engine. This is currently fairly ugly and inefficient. Additionally, it's easy to forget to set the original TS in some edge cases. For example, #255 included a fix for IC3IA where the original TS was lost. This is because it passes a fresh TS as the "main" one because that is the abstraction that other members needed access to right away (e.g. the abstractor classes) for modifying it. But then the orig_ts_ was not set correctly so we had to manually do that. But there's no infrastructure for ensuring that happens properly.

Link error when building in github actions environment

Here's an example log: https://github.com/leonardt/fault/runs/1311361414?check_suite_focus=true

Since the undefined references involved string methods, I thought it might be related to -D_GLIBCXX_USE_CXX11_ABI=0. However from what I can tell, the coreir release being used is built on travis with gcc-7 without setting that define, and when I forced gcc-8 on github actions, still got the same error. One thing I haven't tried is building pono with -D_GLIBCXX_USE_CXX11_ABI=0, but given the next finding detailed below, I didn't pursue this.

What's even more confusing: building pono-lib works (linking coreir), but building the pono executable (which links pono-lib) fails with the linker errors, so that makes me think it's not related to the string ABI problems. I poked around and still couldn't seem to resolve the issue. This process seems to work fine on the pono travis environment, as well as my local macos environment, so I'm guessing it's something different about the github environment. I haven't been able to figure out what might be the cause though.

I did find that it seems that using target_sources (https://github.com/upscale-project/pono/blob/master/CMakeLists.txt#L167) causes the coreir_encoder.cpp file to be rebuilt for the executable. However, even when I changed the cmake logic to just use a SOURCES variable (https://github.com/upscale-project/pono/blob/7777658cbf349892341906ccb8716ab2117eef35/CMakeLists.txt#L157) to avoid the recompilation, I still got linker errors related to coreir (here's an example log: https://github.com/leonardt/fault/runs/1311285582?check_suite_focus=true). (again this recompilation doesn't seem to be problematic for pono travis or my local env)

FWIW: I managed to unblock myself by just building pono-lib since that's actually all I need for my flow, so I don't think this should be high priority until someone else comes along that is blocked by this issue. But I figured it's worth documenting so if it does come up again we have somewhere to start.

Here are the relevant error messages so it may be easier to find this note.

CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o: In function `pono::CoreIREncoder::read_coreir_file(CoreIR::Context*, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >)':
coreir_encoder.cpp:(.text+0x54c): undefined reference to `CoreIR::loadFromFile(CoreIR::Context*, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, CoreIR::Module**)'
CMakeFiles/pono-bin.dir/build.make:125: recipe for target 'pono' failed
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o: In function `pono::CoreIREncoder::process_instance(CoreIR::Instance*)':
CMakeFiles/Makefile2:277: recipe for target 'CMakeFiles/pono-bin.dir/all' failed
coreir_encoder.cpp:(.text+0x87d): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0x8c3): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0xa33): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0xceb): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0xd51): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o:coreir_encoder.cpp:(.text+0xdbb): more undefined references to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)' follow
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o: In function `pono::CoreIREncoder::wire_connection(std::pair<CoreIR::Wireable*, CoreIR::Wireable*>)':
coreir_encoder.cpp:(.text+0x2606): undefined reference to `CoreIR::isNumber(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >)'
coreir_encoder.cpp:(.text+0x2819): undefined reference to `CoreIR::isNumber(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >)'
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o: In function `pono::CoreIREncoder::process_state_element(CoreIR::Instance*)':
coreir_encoder.cpp:(.text+0x30d7): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0x3143): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0x348d): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0x34f3): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0x3565): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o:coreir_encoder.cpp:(.text+0x35c0): more undefined references to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)' follow
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o: In function `pono::CoreIREncoder::encode()':
coreir_encoder.cpp:(.text+0x4a79): undefined reference to `CoreIR::Context::runPasses(std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > >, std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > >)'
coreir_encoder.cpp:(.text+0x573c): undefined reference to `CoreIR::isNumber(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >)'
coreir_encoder.cpp:(.text+0x6185): undefined reference to `CoreIR::isNumber(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >)'
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o: In function `CoreIR::Module::getGenArgs[abi:cxx11]()':
coreir_encoder.cpp:(.text._ZN6CoreIR6Module10getGenArgsB5cxx11Ev[_ZN6CoreIR6Module10getGenArgsB5cxx11Ev]+0x127): undefined reference to `CoreIR::GlobalValue::getRefName[abi:cxx11]() const'
collect2: error: ld returned 1 exit status

libpono.so: undefined reference to `CoreIR::GlobalValue::getRefName[abi:cxx11]() const'
libpono.so: undefined reference to `CoreIR::Context::runPasses(std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > >, std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > >)'
CMakeFiles/pono-bin.dir/build.make:110: recipe for target 'pono' failed
libpono.so: undefined reference to `CoreIR::loadFromFile(CoreIR::Context*, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, CoreIR::Module**)'
CMakeFiles/Makefile2:277: recipe for target 'CMakeFiles/pono-bin.dir/all' failed
libpono.so: undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
libpono.so: undefined reference to `CoreIR::isNumber(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >)'

Copy TransitionSystem to Property

Edit the transition system in place if

we need to introduce witnesses (currently done in the encoder)
for COI
for property-based abstractions

Unwanted skbuild printouts

When i import skbuild with python3 on my system I get the following printouts:

>>> import skbuild
Generating grammar tables from /usr/lib/python3.8/lib2to3/Grammar.txt
Generating grammar tables from /usr/lib/python3.8/lib2to3/PatternGrammar.txt

This causes issues in python/CMakeLists.txt since line 90 is not expecting this extra printout.

Locally, I have fixed this by replacing the import skbuild at line 81 of the script with import sys; temp = sys.stdout; sys.stdout = open(os.devnull,\"w\"); import skbuild; sys.stdout = temp to silence the output.

Build broken with latest smt-switch

Looks like stanford-centaur/smt-switch@4858959 broke cosa2 build. This worked as a quick-and-dirty work-around for me:

diff --git a/contrib/setup-smt-switch.sh b/contrib/setup-smt-switch.sh
index e22cde1..694d4ba 100755
--- a/contrib/setup-smt-switch.sh
+++ b/contrib/setup-smt-switch.sh
@@ -51,6 +51,7 @@ if [ ! -d "$DEPS/smt-switch" ]; then
     cd $DEPS
     git clone https://github.com/makaimann/smt-switch
     cd smt-switch
+    git checkout -f 48589590~1
     ./contrib/setup-btor.sh
 
     if [[ "$WITH_MSAT" != default ]]; then

cc @makaimann

Handle state variables without next-function as inputs

Issue refers to BTOR2 inputs and Pono master 5b6af14.

Excerpt from the BTOR2 paper (https://link.springer.com/content/pdf/10.1007%2F978-3-319-96145-3_32.pdf):

"A state variable without associated next function is treated as a primary input, i.e., it has the same behaviour as inputs defined via keyword input."

Pono properly handles inputs that are explicitly declared using the keyword input. Such inputs are added to the set inputvars_ of a transition system.

However, state variables declared using the keyword state and for which no next-function is given are added to the set statevars_ of a transition system although according to the BTOR2 standard they should appear in inputvars_.

Segfault in CVC4 when copying default transition system

This bug could be in smt-switch or CVC4 as well, because this doesn't occur when I tried switching the default solver to MathSAT. It's unclear at this point where exactly the problem is.

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.