Skip to content

Commit

Permalink
Remove debug and redundant functions
Browse files Browse the repository at this point in the history
  • Loading branch information
arranf committed Dec 1, 2017
1 parent dd402a9 commit 882076c
Showing 1 changed file with 1 addition and 20 deletions.
21 changes: 1 addition & 20 deletions src/Expr.js
Original file line number Diff line number Diff line change
Expand Up @@ -76,20 +76,6 @@ class Expr {
return Number(numeralDecString);
}

// TODO (AF) Replace this, this is horrid
parseNumber() {
let numString = this.toString();
if (numString.includes('seq')) {
const regex = /Expr {\(seq.unit ([\d\.]+)\)}/g;
const matches = regex.exec(numString)
// console.log('Match is ' + matches[1])
if (matches.length > 1){
return Number(matches[1])
}
throw new Exception(`Unable to parse number from ${numString}`)
}
}

getAstSortKind() {
return Z3.Z3_get_sort_kind(this.context.ctx, Z3.Z3_get_sort(this.context.ctx, this.ast));
}
Expand All @@ -101,12 +87,10 @@ class Expr {

// Use this to get the value at the index of an array
selectFromIndex(index) {
let result = this.context.mkSelect(this, index);
return result;
return this.context.mkSelect(this, index);
}

asConstant(model) {
console.log('Entering As Constant')
switch (this.getAstSortKind()) {

case Z3.INT_SORT:
Expand All @@ -127,8 +111,6 @@ class Expr {
}

case Z3.ARRAY_SORT: {
console.log(this);
console.log(`This length ${this.length}`)
const arrayLength = model.eval(this.length).asConstant(model);
let array = [];

Expand All @@ -146,7 +128,6 @@ class Expr {
return undefined;
}
}
console.log('Exiting As Constant')
}

simplify() {
Expand Down

0 comments on commit 882076c

Please sign in to comment.